:: Oriented Metric-Affine Plane - Part II :: by Jaros{\l}aw Zajkowski :: :: Received June 19, 1992 :: Copyright (c) 1992-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RLVECT_1, XBOOLE_0, ANALOAF, SUBSET_1, ANALMETR, ANALORT, STRUCT_0, SYMSP_1, DIRORT; notations STRUCT_0, RLVECT_1, ANALOAF, ANALMETR, ANALORT; constructors ANALMETR, ANALORT; registrations ANALOAF, ANALORT, ANALMETR; theorems ANALMETR, ANALORT; begin reserve V for RealLinearSpace; reserve x,y for VECTOR of V; notation let AS be non empty OrtStr; let a,b,c,d be Element of AS; synonym a,b '//' c,d for a,b _|_ c,d; end; theorem Th1: Gen x,y implies (for u,u1,v,v1,w being Element of CESpace(V,x,y) holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u))) & (for u,v,w being Element of CESpace(V,x,y) holds ex u1 being Element of CESpace(V,x,y) st w<>u1 & w,u1 '//' u,v ) & for u,v,w being Element of CESpace(V,x,y) holds ex u1 being Element of CESpace(V,x,y) st w<>u1 & u,v '//' w,u1 proof assume A1: Gen x,y; set S=CESpace(V,x,y); A2: S= OrtStr (# the carrier of V,CORTE(V,x,y) #) by ANALORT:def 7; thus for u,u1,v,v1,w being Element of S holds u,u '//' v,w & u,v '//' w,w & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u) proof let u,u1,v,v1,w be Element of S; reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1 as Element of V by A2; u9,u9,v9,w9 are_COrte_wrt x,y by ANALORT:20; hence u,u '//' v,w by ANALORT:54; u9,v9,w9,w9 are_COrte_wrt x,y by ANALORT:22; hence u,v '//' w,w by ANALORT:54; u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,v19,u19 are_COrte_wrt x,y implies u9=v9 or u19=v19 by A1,ANALORT:30; hence u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1 by ANALORT:54; u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,u19,w9 are_COrte_wrt x,y implies u9,v9,v19,w9 are_COrte_wrt x,y or u9,v9,w9,v19 are_COrte_wrt x,y by A1, ANALORT:32; hence u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1 by ANALORT:54; u9,v9,u19,v19 are_COrte_wrt x,y implies v9,u9,v19,u19 are_COrte_wrt x ,y by ANALORT:34; hence u,v '//' u1,v1 implies v,u '//' v1,u1 by ANALORT:54; u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,v19,w9 are_COrte_wrt x,y implies u9,v9,u19,w9 are_COrte_wrt x,y by A1,ANALORT:36; hence u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w by ANALORT:54; u9,u19,v9,v19 are_COrte_wrt x,y implies v9,v19,u9,u19 are_COrte_wrt x ,y or v9,v19,u19,u9 are_COrte_wrt x,y by A1,ANALORT:18; hence u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u by ANALORT:54 ; end; thus for u,v,w being Element of S holds ex u1 being Element of S st w<>u1 & w,u1 '//' u,v proof let u,v,w be Element of S; reconsider u9=u,v9=v,w9=w as Element of V by A2; consider u19 being Element of V such that A3: w9<>u19 and A4: w9,u19,u9,v9 are_COrte_wrt x,y by A1,ANALORT:38; reconsider u1=u19 as Element of S by A2; w,u1 '//' u,v by A4,ANALORT:54; hence thesis by A3; end; let u,v,w be Element of S; reconsider u9=u,v9=v,w9=w as Element of V by A2; consider u19 being Element of V such that A5: w9<>u19 and A6: u9,v9,w9,u19 are_COrte_wrt x,y by A1,ANALORT:40; reconsider u1=u19 as Element of S by A2; u,v '//' w,u1 by A6,ANALORT:54; hence thesis by A5; end; theorem Th2: Gen x,y implies (for u,u1,v,v1,w being Element of CMSpace(V,x,y) holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u))) & (for u,v,w being Element of CMSpace(V,x,y) holds ex u1 being Element of CMSpace(V,x,y) st w<>u1 & w,u1 '//' u,v ) & for u,v,w being Element of CMSpace(V,x,y) holds ex u1 being Element of CMSpace(V,x,y) st w<>u1 & u,v '//' w,u1 proof assume A1: Gen x,y; set S=CMSpace(V,x,y); A2: S= OrtStr(# the carrier of V,CORTM(V,x,y) #) by ANALORT:def 8; thus for u,u1,v,v1,w being Element of S holds u,u '//' v,w & u,v '//' w,w & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u) proof let u,u1,v,v1,w be Element of S; reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1 as Element of V by A2; u9,u9,v9,w9 are_COrtm_wrt x,y by ANALORT:21; hence u,u '//' v,w by ANALORT:55; u9,v9,w9,w9 are_COrtm_wrt x,y by ANALORT:23; hence u,v '//' w,w by ANALORT:55; u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,v19,u19 are_COrtm_wrt x,y implies u9=v9 or u19=v19 by A1,ANALORT:31; hence u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1 by ANALORT:55; u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,u19,w9 are_COrtm_wrt x,y implies u9,v9,v19,w9 are_COrtm_wrt x,y or u9,v9,w9,v19 are_COrtm_wrt x,y by A1, ANALORT:33; hence u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1 by ANALORT:55; u9,v9,u19,v19 are_COrtm_wrt x,y implies v9,u9,v19,u19 are_COrtm_wrt x ,y by ANALORT:35; hence u,v '//' u1,v1 implies v,u '//' v1,u1 by ANALORT:55; u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,v19,w9 are_COrtm_wrt x,y implies u9,v9,u19,w9 are_COrtm_wrt x,y by A1,ANALORT:37; hence u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w by ANALORT:55; u9,u19,v9,v19 are_COrtm_wrt x,y implies v9,v19,u9,u19 are_COrtm_wrt x , y or v9,v19,u19,u9 are_COrtm_wrt x,y by A1,ANALORT:19; hence u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u by ANALORT:55 ; end; thus for u,v,w being Element of S holds ex u1 being Element of S st w<>u1 & w,u1 '//' u,v proof let u,v,w be Element of S; reconsider u9=u,v9=v,w9=w as Element of V by A2; consider u19 being Element of V such that A3: w9<>u19 and A4: w9,u19,u9,v9 are_COrtm_wrt x,y by A1,ANALORT:39; reconsider u1=u19 as Element of S by A2; w,u1 '//' u,v by A4,ANALORT:55; hence thesis by A3; end; let u,v,w be Element of S; reconsider u9=u,v9=v,w9=w as Element of V by A2; consider u19 being Element of V such that A5: w9<>u19 and A6: u9,v9,w9,u19 are_COrtm_wrt x,y by A1,ANALORT:41; reconsider u1=u19 as Element of S by A2; u,v '//' w,u1 by A6,ANALORT:55; hence thesis by A5; end; definition let IT be non empty OrtStr; attr IT is Oriented_Orthogonality_Space-like means :Def1: (for u,u1,v,v1,w being Element of IT holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u, v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v ,v1 '//' u,u1 or v,v1 '//' u1,u))) & (for u,v,w being Element of IT holds ex u1 being Element of IT st w<>u1 & w,u1 '//' u,v ) & for u,v,w being Element of IT holds ex u1 being Element of IT st w<>u1 & u,v '//' w,u1; end; registration cluster Oriented_Orthogonality_Space-like for non empty OrtStr; existence proof consider V,x,y such that A1: Gen x,y by ANALMETR:3; take C = CESpace(V,x,y); thus (for u,u1,v,v1,w being Element of C holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w ) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u))) & (for u,v,w being Element of C holds ex u1 being Element of C st w<>u1 & w,u1 '//' u,v ) & for u,v,w being Element of C holds ex u1 being Element of C st w<>u1 & u,v '//' w,u1 by A1,Th1; end; end; definition mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like non empty OrtStr; end; theorem Th3: Gen x,y implies CMSpace(V,x,y) is Oriented_Orthogonality_Space proof assume A1: Gen x,y; then A2: for u,v,w being Element of CMSpace(V,x,y) holds ex u1 being Element of CMSpace(V,x,y) st w<>u1 & w,u1 '//' u,v by Th2; A3: for u,v,w being Element of CMSpace(V,x,y) holds ex u1 being Element of CMSpace(V,x,y) st w<>u1 & u,v '//' w,u1 by A1,Th2; for u,u1,v,v1,w,w1,w2 being Element of CMSpace(V,x,y) holds u,u '//' v,w & u,v '//' w,w & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u, v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u) by A1 ,Th2; hence thesis by A2,A3,Def1; end; theorem Th4: Gen x,y implies CESpace(V,x,y) is Oriented_Orthogonality_Space proof assume A1: Gen x,y; then A2: for u,v,w being Element of CESpace(V,x,y) holds ex u1 being Element of CESpace(V,x,y) st w<>u1 & w,u1 '//' u,v by Th1; A3: for u,v,w being Element of CESpace(V,x,y) holds ex u1 being Element of CESpace(V,x,y) st w<>u1 & u,v '//' w,u1 by A1,Th1; for u,u1,v,v1,w,w1,w2 being Element of CESpace(V,x,y) holds u,u '//' v,w & u,v '//' w,w & (u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1) & (u, v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u) by A1 ,Th1; hence thesis by A2,A3,Def1; end; reserve AS for Oriented_Orthogonality_Space; reserve u,u1,u2,u3,v,v1,v2,v3,w,w1 for Element of AS; theorem for u,v,w being Element of AS holds ex u1 being Element of AS st u1,w '//' u,v & u1<>w proof let u,v,w; consider u1 such that A1: u1<>w and A2: w,u1 '//' v,u by Def1; u1,w '//' u,v by A2,Def1; hence thesis by A1; end; theorem for u,v,w being Element of AS holds ex u1 being Element of AS st u<>u1 & (v,w '//' u,u1 or v,w '//' u1,u) proof let u,v,w; consider u1 such that A1: u<>u1 and A2: u,u1 '//' v,w by Def1; v,w '//' u,u1 or v,w '//' u1,u by A2,Def1; hence thesis by A1; end; definition let AS be Oriented_Orthogonality_Space; let a,b,c,d be Element of AS; pred a,b _|_ c,d means a,b '//' c,d or a,b '//' d,c; end; definition let AS be Oriented_Orthogonality_Space; let a,b,c,d be Element of AS; pred a,b // c,d means ex e,f being Element of AS st e<>f & e,f '//' a ,b & e,f '//' c,d; end; definition let IT be Oriented_Orthogonality_Space; attr IT is bach_transitive means for u,u1,u2,v,v1,v2,w,w1 being Element of IT holds ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=v1 or u,u1 '//' u2,v2) ); end; definition let IT be Oriented_Orthogonality_Space; attr IT is right_transitive means for u,u1,u2,v,v1,v2,w,w1 being Element of IT holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2) ); end; definition let IT be Oriented_Orthogonality_Space; attr IT is left_transitive means for u,u1,u2,v,v1,v2,w,w1 being Element of IT holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1) ); end; definition let IT be Oriented_Orthogonality_Space; attr IT is Euclidean_like means for u,u1,v,v1 being Element of IT holds (u,u1 '//' v,v1 implies v,v1 '//' u1,u ); end; definition let IT be Oriented_Orthogonality_Space; attr IT is Minkowskian_like means for u,u1,v,v1 being Element of IT holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 ); end; theorem u,u1 // w,w & w,w // u,u1 proof set v = the Element of AS; consider v1 such that A1: v1<>v and A2: v,v1 '//' u,u1 by Def1; v,v1 '//' w,w by Def1; hence thesis by A1,A2; end; theorem u,u1 // v,v1 implies v,v1 // u,u1; theorem u,u1 // v,v1 implies u1,u // v1,v proof assume u,u1 // v,v1; then consider w,w1 such that A1: w<>w1 and A2: w,w1 '//' u,u1 and A3: w,w1 '//' v,v1; A4: w1,w '//' v1,v by A3,Def1; w1,w '//' u1,u by A2,Def1; hence thesis by A1,A4; end; theorem AS is left_transitive iff for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v ,v1 '//' w,w1 & v<>v1 implies u2,v2 '//' w,w1) proof A1: (for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v,v1 '//' w,w1 & v<>v1 implies u2,v2 '//' w,w1)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1) ) proof assume A2: for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v,v1 '//' w,w1 & v<>v1 implies u2,v2 '//' w,w1); let u,u1,u2,v,v1,v2,w,w1; assume that A3: u,u1 '//' v,v1 and A4: v,v1 '//' w,w1 and A5: u,u1 '//' u2,v2; now assume that A6: u<>u1 and v<>v1; v,v1 // u2,v2 by A3,A5,A6; hence thesis by A2,A4; end; hence thesis; end; thus thesis by A1; end; theorem AS is bach_transitive iff for u,u1,u2,v,v1,v2 holds (u,u1 '//' v ,v1 & v,v1 // u2,v2 & v<>v1 implies u,u1 '//' u2,v2) proof A1: (for u,u1,u2,v,v1,v2 holds (u,u1 '//' v,v1 & v,v1 // u2,v2 & v<>v1 implies u,u1 '//' u2,v2)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=v1 or u,u1 '//' u2,v2) ) proof assume A2: for u,u1,u2,v,v1,v2 holds (u,u1 '//' v,v1 & v,v1 // u2,v2 & v<>v1 implies u,u1 '//' u2,v2); let u,u1,u2,v,v1,v2,w,w1; assume that A3: u,u1 '//' v,v1 and A4: w,w1 '//' v,v1 and A5: w,w1 '//' u2,v2; now assume that A6: w<>w1 and v<>v1; v,v1 // u2,v2 by A4,A5,A6; hence thesis by A2,A3; end; hence thesis; end; thus thesis by A1; end; theorem AS is bach_transitive implies for u,u1,v,v1,w,w1 holds (u,u1 // v,v1 & v,v1 // w,w1 & v<>v1 implies u,u1 // w,w1) proof assume A1: AS is bach_transitive; let u,u1,v,v1,w,w1; assume that A2: u,u1 // v,v1 and A3: v,v1 // w,w1 and A4: v<>v1; consider v2,v3 such that A5: v2<>v3 and A6: v2,v3 '//' u,u1 and A7: v2,v3 '//' v,v1 by A2; v2,v3 '//' w,w1 by A1,A3,A4,A7; hence thesis by A5,A6; end; theorem Th13: Gen x,y & AS=CESpace(V,x,y) implies AS is Euclidean_like left_transitive right_transitive bach_transitive proof assume that A1: Gen x,y and A2: AS=CESpace(V,x,y); A3: CESpace(V,x,y)=OrtStr (# the carrier of V,CORTE(V,x,y) #) by ANALORT:def 7; A4: now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v= v1 or u,u1 '//' u2,v2 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y & u29,v29,w9,w19 are_COrte_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29 are_COrte_wrt x,y) by A1,ANALORT:44; hence thesis by A2,ANALORT:54; end; end; A5: now let u,u1,v,v1 be Element of AS; thus u,u1 '//' v,v1 implies v,v1 '//' u1,u proof reconsider u9=u,v9=v,u19=u1,v19=v1 as Element of V by A2,A3; u9,u19,v9,v19 are_COrte_wrt x,y implies v9,v19,u19,u9 are_COrte_wrt x,y by A1,ANALORT:18; hence thesis by A2,ANALORT:54; end; end; A6: now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v= v1 or u2,v2 '//' w,w1 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y & u9,u19,u29,v29 are_COrte_wrt x,y implies (u9=u19 or v9=v19 or u29,v29,w9,w19 are_COrte_wrt x,y) by A1,ANALORT:46; hence thesis by A2,ANALORT:54; end; end; now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v= v1 or u,u1 '//' u2,v2 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrte_wrt x,y & w9,w19,v9,v19 are_COrte_wrt x,y & w9,w19,u29,v29 are_COrte_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29 are_COrte_wrt x,y) by A1,ANALORT:42; hence thesis by A2,ANALORT:54; end; end; hence thesis by A4,A6,A5; end; registration cluster Euclidean_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space; existence proof consider V,x,y such that A1: Gen x,y by ANALMETR:3; reconsider AS=CESpace(V,x,y) as Oriented_Orthogonality_Space by A1,Th4; take AS; thus thesis by A1,Th13; end; end; theorem Th14: Gen x,y & AS=CMSpace(V,x,y) implies AS is Minkowskian_like left_transitive right_transitive bach_transitive proof assume that A1: Gen x,y and A2: AS=CMSpace(V,x,y); A3: CMSpace(V,x,y)=OrtStr (# the carrier of V,CORTM(V,x,y) #) by ANALORT:def 8; A4: now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v= v1 or u,u1 '//' u2,v2 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y & u29,v29,w9,w19 are_COrtm_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29 are_COrtm_wrt x,y) by A1,ANALORT:45; hence thesis by A2,ANALORT:55; end; end; A5: now let u,u1,v,v1 be Element of AS; thus u,u1 '//' v,v1 implies v,v1 '//' u,u1 proof reconsider u9=u,v9=v,u19=u1,v19=v1 as Element of V by A2,A3; u9,u19,v9,v19 are_COrtm_wrt x,y implies v9,v19,u9,u19 are_COrtm_wrt x,y by A1,ANALORT:19; hence thesis by A2,ANALORT:55; end; end; A6: now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v= v1 or u2,v2 '//' w,w1 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y & u9,u19,u29,v29 are_COrtm_wrt x,y implies (u9=u19 or v9=v19 or u29,v29,w9,w19 are_COrtm_wrt x,y) by A1,ANALORT:47; hence thesis by A2,ANALORT:55; end; end; now let u,u1,u2,v,v1,v2,w,w1 be Element of AS; thus u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v= v1 or u,u1 '//' u2,v2 ) proof reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element of V by A2,A3; u9,u19,v9,v19 are_COrtm_wrt x,y & w9,w19,v9,v19 are_COrtm_wrt x,y & w9,w19,u29,v29 are_COrtm_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29 are_COrtm_wrt x,y) by A1,ANALORT:43; hence thesis by A2,ANALORT:55; end; end; hence thesis by A4,A6,A5; end; registration cluster Minkowskian_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space; existence proof consider V,x,y such that A1: Gen x,y by ANALMETR:3; reconsider AS=CMSpace(V,x,y) as Oriented_Orthogonality_Space by A1,Th3; take AS; thus thesis by A1,Th14; end; end; theorem Th15: AS is left_transitive implies AS is right_transitive proof (for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( (u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 ) implies (u=u1 or v=v1 or u2,v2 '//' w,w1 ))) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & v ,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2 )) proof assume A1: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v, v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1 )); let u,u1,u2,v,v1,v2,w,w1; assume that A2: u,u1 '//' v,v1 and A3: v,v1 '//' w,w1 and A4: u2,v2 '//' w,w1; A5: ( w=w1 or v=v1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2 ) implies (w=w1 or v=v1 or u,u1 '//' u2,v2 ) proof now A6: now assume v2,u2 '//' w,w1; then u2,v2 '//' w1,w by Def1; then u2=v2 or w=w1 by A4,Def1; hence thesis; end; u=u1 implies thesis by Def1; hence thesis by A1,A2,A3,A6; end; hence thesis; end; A7: now assume that A8: w,w1 '//' v,v1 and A9: v,v1 '//' u,u1 and A10: w,w1 '//' v2,u2; w=w1 or v=v1 or v2,u2 '//' u,u1 by A1,A8,A9,A10; hence thesis by A5,Def1; end; A11: now assume that A12: w,w1 '//' v1,v and A13: v,v1 '//' u,u1 and A14: w,w1 '//' v2,u2; v1,v '//' u1,u by A13,Def1; then w=w1 or v=v1 or v2,u2 '//' u1,u by A1,A12,A14; then w=w1 or v=v1 or u2,v2 '//' u,u1 by Def1; hence thesis by A5,Def1; end; A15: now assume that A16: w,w1 '//' v1,v and A17: v,v1 '//' u,u1 and A18: w,w1 '//' u2,v2; v1,v '//' u1,u by A17,Def1; then w=w1 or v=v1 or u2,v2 '//' u1,u by A1,A16,A18; then w=w1 or v=v1 or v2,u2 '//' u,u1 by Def1; hence thesis by A5,Def1; end; A19: now assume that A20: w,w1 '//' v1,v and A21: v,v1 '//' u1,u and A22: w,w1 '//' v2,u2; v1,v '//' u,u1 by A21,Def1; then w=w1 or v=v1 or v2,u2 '//' u,u1 by A1,A20,A22; hence thesis by A5,Def1; end; A23: now assume that A24: w,w1 '//' v1,v and A25: v,v1 '//' u1,u and A26: w,w1 '//' u2,v2; v1,v '//' u,u1 by A25,Def1; then w=w1 or v1=v or u2,v2 '//' u,u1 by A1,A24,A26; hence thesis by A5,Def1; end; A27: now assume that A28: w,w1 '//' v,v1 and A29: v,v1 '//' u1,u and A30: w,w1 '//' v2,u2; w=w1 or v=v1 or v2,u2 '//' u1,u by A1,A28,A29,A30; then w=w1 or v=v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 by Def1; hence thesis by A5,Def1; end; A31: now assume that A32: w,w1 '//' v,v1 and A33: v,v1 '//' u1,u and A34: w,w1 '//' u2,v2; w=w1 or v=v1 or u2,v2 '//' u1,u by A1,A32,A33,A34; then w=w1 or v=v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 by Def1; hence thesis by A5,Def1; end; now assume that A35: w,w1 '//' v,v1 and A36: v,v1 '//' u,u1 and A37: w,w1 '//' u2,v2; w=w1 or v=v1 or u2,v2 '//' u,u1 by A1,A35,A36,A37; hence thesis by A5,Def1; end; hence thesis by A2,A3,A4,A7,A31,A27,A15,A11,A23,A19,Def1; end; hence thesis; end; theorem AS is left_transitive implies AS is bach_transitive proof (for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( (u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 ) implies (u=u1 or v=v1 or u2,v2 '//' w,w1 ))) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & w ,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=v1 or u,u1 '//' u2,v2)) proof assume A1: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v, v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1 )); let u,u1,u2,v,v1,v2,w,w1; A2: AS is left_transitive implies AS is right_transitive by Th15; then A3: u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w implies thesis by A1; assume that A4: u,u1 '//' v,v1 and A5: w,w1 '//' v,v1 and A6: w,w1 '//' u2,v2; A7: ( v=v1 or w=w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2) implies (w=w1 or v=v1 or u,u1 '//' u2,v2) proof A8: now assume that A9: u,u1 '//' v2,u2 and A10: u<>u1 and A11: v<>v1 and w<>w1; A12: now assume A13: u2,v2 '//' u,u1; then A14: u2,v2 '//' w,w1 by A2,A1,A4,A5,A10,A11; A15: now assume u2,v2 '//' w1,w; then w=w1 or u2=v2 by A14,Def1; hence thesis; end; w1,w '//' v2,u2 by A6,Def1; then u2,v2 '//' w1,w or u2=v2 by A2,A1,A9,A10,A13; hence thesis by A15; end; A16: now A17: w1,w '//' v1,v by A5,Def1; assume A18: u2,v2 '//' u1,u; u1,u '//' v1,v by A4,Def1; then A19: u2,v2 '//' w1,w by A2,A1,A10,A11,A18,A17; A20: now assume u2,v2 '//' w,w1; then w=w1 or u2=v2 by A19,Def1; hence thesis; end; u1,u '//' u2,v2 by A9,Def1; then u2,v2 '//' w,w1 or u2=v2 by A2,A1,A6,A10,A18; hence thesis by A20; end; v2,u2 '//' u,u1 or v2,u2 '//' u1,u by A9,Def1; hence thesis by A16,A12,Def1; end; assume v=v1 or w=w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2; hence thesis by A8,Def1; end; A21: now assume that A22: u,u1 '//' v,v1 and A23: v,v1 '//' w,w1 and A24: u2,v2 '//' w1,w; v2,u2 '//' w,w1 by A24,Def1; hence thesis by A2,A1,A7,A22,A23; end; A25: now assume that A26: u,u1 '//' v,v1 and A27: v,v1 '//' w1,w and A28: u2,v2 '//' w,w1; v2,u2 '//' w1,w by A28,Def1; hence thesis by A2,A1,A7,A26,A27; end; u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies thesis by A2,A1; hence thesis by A4,A5,A6,A21,A3,A25,Def1; end; hence thesis; end; theorem AS is bach_transitive implies (AS is right_transitive iff for u,u1,v, v1,u2,v2 holds ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2 implies u,u1 // v, v1) ) proof A1: (for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ((u,u1 '//' v,v1 & v ,v1 '//' w,w1 & u2,v2 '//' w,w1 ) implies (w=w1 or v=v1 or u,u1 '//' u2,v2 ))) implies for u,u1,v,v1,u2,v2 holds ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2 implies u,u1 // v,v1) proof set w = the Element of AS; assume A2: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2 ); let u,u1,v,v1,u2,v2; assume that A3: u,u1 '//' u2,v2 and A4: v,v1 '//' u2,v2 and A5: u2<>v2; consider w1 such that A6: w<>w1 and A7: w,w1 '//' u,u1 by Def1; A8: now set w = the Element of AS; assume A9: u=u1; consider w1 such that A10: w<>w1 and A11: w,w1 '//' v,v1 by Def1; w,w1 '//' u,u by Def1; hence thesis by A9,A10,A11; end; now assume u<>u1; then w,w1 '//' v,v1 by A2,A3,A4,A5,A7; hence thesis by A6,A7; end; hence thesis by A8; end; assume A12: AS is bach_transitive; (for u,u1,v,v1,u2,v2 holds ((u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2 ) implies u,u1 // v,v1)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2 )) proof assume A13: for u,u1,v,v1,u2,v2 holds u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <>v2 implies u,u1 // v,v1; let u,u1,u2,v,v1,v2,w,w1; assume that A14: u,u1 '//' v,v1 and A15: v,v1 '//' w,w1 and A16: u2,v2 '//' w,w1; now assume that A17: w<>w1 and v<>v1; v,v1 // u2,v2 by A13,A15,A16,A17; then ex u3,v3 st u3<>v3 & u3,v3 '//' v,v1 & u3,v3 '//' u2,v2; hence thesis by A12,A14; end; hence thesis; end; hence thesis by A1; end; theorem AS is right_transitive & (AS is Euclidean_like or AS is Minkowskian_like) implies AS is left_transitive proof assume A1: AS is right_transitive; (for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 ) or for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1 '//' u1,u )) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2, v2 '//' w,w1 )) proof assume A2: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v, v1 '//' u,u1 ) or for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1 '//' u1,u ); let u,u1,u2,v,v1,v2,w,w1; assume that A3: u,u1 '//' v,v1 and A4: v,v1 '//' w,w1 and A5: u,u1 '//' u2,v2; A6: now assume A7: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1 '//' u1,u ); now w,w1 '//' v1,v by A4,A7; then A8: w1,w '//' v,v1 by Def1; A9: u2,v2 '//' u1,u by A5,A7; assume that A10: u<>u1 and A11: v<>v1; v,v1 '//' u1,u by A3,A7; then w1,w '//' u2,v2 by A1,A10,A11,A8,A9; hence thesis by A7; end; hence thesis; end; now assume A12: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 ); now A13: u2,v2 '//' u,u1 by A5,A12; A14: w,w1 '//' v,v1 by A4,A12; assume that A15: u<>u1 and A16: v<>v1; v,v1 '//' u,u1 by A3,A12; then w,w1 '//' u2,v2 by A1,A15,A16,A14,A13; hence thesis by A12; end; hence thesis; end; hence thesis by A2,A6; end; hence thesis; end;