:: Oriented Metric-Affine Plane - Part II :: by Jaros{\l}aw Zajkowski :: :: Received June 19, 1992 :: Copyright (c) 1992-2016 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; 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 :: DIRORT:1 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; theorem :: DIRORT:2 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; definition let IT be non empty OrtStr; attr IT is Oriented_Orthogonality_Space-like means :: DIRORT:def 1 (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; end; definition mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like non empty OrtStr; end; theorem :: DIRORT:3 Gen x,y implies CMSpace(V,x,y) is Oriented_Orthogonality_Space; theorem :: DIRORT:4 Gen x,y implies CESpace(V,x,y) is Oriented_Orthogonality_Space; reserve AS for Oriented_Orthogonality_Space; reserve u,u1,u2,u3,v,v1,v2,v3,w,w1 for Element of AS; theorem :: DIRORT:5 for u,v,w being Element of AS holds ex u1 being Element of AS st u1,w '//' u,v & u1<>w; theorem :: DIRORT:6 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); definition let AS be Oriented_Orthogonality_Space; let a,b,c,d be Element of AS; pred a,b _|_ c,d means :: DIRORT:def 2 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 :: DIRORT:def 3 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 :: DIRORT:def 4 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 :: DIRORT:def 5 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 :: DIRORT:def 6 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 :: DIRORT:def 7 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 :: DIRORT:def 8 for u,u1,v,v1 being Element of IT holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 ); end; theorem :: DIRORT:7 u,u1 // w,w & w,w // u,u1; theorem :: DIRORT:8 u,u1 // v,v1 implies v,v1 // u,u1; theorem :: DIRORT:9 u,u1 // v,v1 implies u1,u // v1,v; theorem :: DIRORT:10 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); theorem :: DIRORT:11 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); theorem :: DIRORT:12 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); theorem :: DIRORT:13 Gen x,y & AS=CESpace(V,x,y) implies AS is Euclidean_like left_transitive right_transitive bach_transitive; registration cluster Euclidean_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space; end; theorem :: DIRORT:14 Gen x,y & AS=CMSpace(V,x,y) implies AS is Minkowskian_like left_transitive right_transitive bach_transitive; registration cluster Minkowskian_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space; end; theorem :: DIRORT:15 AS is left_transitive implies AS is right_transitive; theorem :: DIRORT:16 AS is left_transitive implies AS is bach_transitive; theorem :: DIRORT:17 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) ); theorem :: DIRORT:18 AS is right_transitive & (AS is Euclidean_like or AS is Minkowskian_like) implies AS is left_transitive;