:: Oriented Metric-Affine Plane - Part II :: by Jaros{\l}aw Zajkowski :: :: Received June 19, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin notation let AS be non empty AffinStruct ; let a, b, c, d be Element of AS; synonym a,b '//' c,d for a,b // c,d; end; theorem Th1: :: DIRORT:1 for V being RealLinearSpace for x, y being VECTOR of V st Gen x,y holds ( ( 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 & not u = v implies u1 = v1 ) & ( u,v '//' u1,v1 & u,v '//' u1,w & not u,v '//' v1,w implies 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 ) & ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u ) ) ) & ( for u, v, w being Element of (CESpace (V,x,y)) 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)) ex u1 being Element of (CESpace (V,x,y)) st ( w <> u1 & u,v '//' w,u1 ) ) ) proofend; theorem Th2: :: DIRORT:2 for V being RealLinearSpace for x, y being VECTOR of V st Gen x,y holds ( ( 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 & not u = v implies u1 = v1 ) & ( u,v '//' u1,v1 & u,v '//' u1,w & not u,v '//' v1,w implies 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 ) & ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u ) ) ) & ( for u, v, w being Element of (CMSpace (V,x,y)) 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)) ex u1 being Element of (CMSpace (V,x,y)) st ( w <> u1 & u,v '//' w,u1 ) ) ) proofend; definition let IT be non empty AffinStruct ; attrIT is Oriented_Orthogonality_Space-like means :Def1: :: 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 & not u = v implies u1 = v1 ) & ( u,v '//' u1,v1 & u,v '//' u1,w & not u,v '//' v1,w implies 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 ) & ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u ) ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st ( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st ( w <> u1 & u,v '//' w,u1 ) ) ); end; :: deftheorem Def1 defines Oriented_Orthogonality_Space-like DIRORT:def_1_:_ for IT being non empty AffinStruct holds ( IT is Oriented_Orthogonality_Space-like iff ( ( 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 & not u = v implies u1 = v1 ) & ( u,v '//' u1,v1 & u,v '//' u1,w & not u,v '//' v1,w implies 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 ) & ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u ) ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st ( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st ( w <> u1 & u,v '//' w,u1 ) ) ) ); registration cluster non empty Oriented_Orthogonality_Space-like for AffinStruct ; existence ex b1 being non empty AffinStruct st b1 is Oriented_Orthogonality_Space-like proofend; end; definition mode Oriented_Orthogonality_Space is non empty Oriented_Orthogonality_Space-like AffinStruct ; end; theorem Th3: :: DIRORT:3 for V being RealLinearSpace for x, y being VECTOR of V st Gen x,y holds CMSpace (V,x,y) is Oriented_Orthogonality_Space proofend; theorem Th4: :: DIRORT:4 for V being RealLinearSpace for x, y being VECTOR of V st Gen x,y holds CESpace (V,x,y) is Oriented_Orthogonality_Space proofend; theorem :: DIRORT:5 for AS being Oriented_Orthogonality_Space for u, v, w being Element of AS ex u1 being Element of AS st ( u1,w '//' u,v & u1 <> w ) proofend; theorem :: DIRORT:6 for AS being Oriented_Orthogonality_Space for u, v, w being Element of AS ex u1 being Element of AS st ( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) ) proofend; definition let AS be Oriented_Orthogonality_Space; let a, b, c, d be Element of AS; preda,b _|_ c,d means :: DIRORT:def 2 ( a,b '//' c,d or a,b '//' d,c ); end; :: deftheorem defines _|_ DIRORT:def_2_:_ for AS being Oriented_Orthogonality_Space for a, b, c, d being Element of AS holds ( a,b _|_ c,d iff ( a,b '//' c,d or a,b '//' d,c ) ); definition let AS be Oriented_Orthogonality_Space; let a, b, c, d be Element of AS; preda,b // c,d means :Def3: :: DIRORT:def 3 ex e, f being Element of AS st ( e <> f & e,f '//' a,b & e,f '//' c,d ); end; :: deftheorem Def3 defines // DIRORT:def_3_:_ for AS being Oriented_Orthogonality_Space for a, b, c, d being Element of AS holds ( a,b // c,d iff ex e, f being Element of AS st ( e <> f & e,f '//' a,b & e,f '//' c,d ) ); definition let IT be Oriented_Orthogonality_Space; attrIT is bach_transitive means :Def4: :: DIRORT:def 4 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds u,u1 '//' u2,v2; end; :: deftheorem Def4 defines bach_transitive DIRORT:def_4_:_ for IT being Oriented_Orthogonality_Space holds ( IT is bach_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds u,u1 '//' u2,v2 ); definition let IT be Oriented_Orthogonality_Space; attrIT is right_transitive means :Def5: :: DIRORT:def 5 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds u,u1 '//' u2,v2; end; :: deftheorem Def5 defines right_transitive DIRORT:def_5_:_ for IT being Oriented_Orthogonality_Space holds ( IT is right_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds u,u1 '//' u2,v2 ); definition let IT be Oriented_Orthogonality_Space; attrIT is left_transitive means :Def6: :: DIRORT:def 6 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds u2,v2 '//' w,w1; end; :: deftheorem Def6 defines left_transitive DIRORT:def_6_:_ for IT being Oriented_Orthogonality_Space holds ( IT is left_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds u2,v2 '//' w,w1 ); definition let IT be Oriented_Orthogonality_Space; attrIT is Euclidean_like means :Def7: :: DIRORT:def 7 for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds v,v1 '//' u1,u; end; :: deftheorem Def7 defines Euclidean_like DIRORT:def_7_:_ for IT being Oriented_Orthogonality_Space holds ( IT is Euclidean_like iff for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds v,v1 '//' u1,u ); definition let IT be Oriented_Orthogonality_Space; attrIT is Minkowskian_like means :Def8: :: DIRORT:def 8 for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds v,v1 '//' u,u1; end; :: deftheorem Def8 defines Minkowskian_like DIRORT:def_8_:_ for IT being Oriented_Orthogonality_Space holds ( IT is Minkowskian_like iff for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds v,v1 '//' u,u1 ); theorem :: DIRORT:7 for AS being Oriented_Orthogonality_Space for u, u1, w being Element of AS holds ( u,u1 // w,w & w,w // u,u1 ) proofend; theorem :: DIRORT:8 for AS being Oriented_Orthogonality_Space for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds v,v1 // u,u1 proofend; theorem :: DIRORT:9 for AS being Oriented_Orthogonality_Space for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds u1,u // v1,v proofend; theorem :: DIRORT:10 for AS being Oriented_Orthogonality_Space holds ( AS is left_transitive iff for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds u2,v2 '//' w,w1 ) proofend; theorem Th11: :: DIRORT:11 for AS being Oriented_Orthogonality_Space holds ( AS is bach_transitive iff for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds u,u1 '//' u2,v2 ) proofend; theorem :: DIRORT:12 for AS being Oriented_Orthogonality_Space st AS is bach_transitive holds for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds u,u1 // w,w1 proofend; theorem Th13: :: DIRORT:13 for V being RealLinearSpace for x, y being VECTOR of V for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) proofend; registration cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Euclidean_like for AffinStruct ; existence ex b1 being Oriented_Orthogonality_Space st ( b1 is Euclidean_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive ) proofend; end; theorem Th14: :: DIRORT:14 for V being RealLinearSpace for x, y being VECTOR of V for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CMSpace (V,x,y) holds ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) proofend; registration cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Minkowskian_like for AffinStruct ; existence ex b1 being Oriented_Orthogonality_Space st ( b1 is Minkowskian_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive ) proofend; end; theorem Th15: :: DIRORT:15 for AS being Oriented_Orthogonality_Space st AS is left_transitive holds AS is right_transitive proofend; theorem :: DIRORT:16 for AS being Oriented_Orthogonality_Space st AS is left_transitive holds AS is bach_transitive proofend; theorem :: DIRORT:17 for AS being Oriented_Orthogonality_Space st AS is bach_transitive holds ( AS is right_transitive iff for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds u,u1 // v,v1 ) proofend; theorem :: DIRORT:18 for AS being Oriented_Orthogonality_Space st AS is right_transitive & ( AS is Euclidean_like or AS is Minkowskian_like ) holds AS is left_transitive proofend;