:: Oriented Metric-Affine Plane - Part II
:: by Jaros{\l}aw Zajkowski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users


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: :: 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 ) ) )
proof end;

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 ) ) )
proof end;

definition
let IT be non empty OrtStr ;
attr IT 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 OrtStr 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 OrtStr ;
existence
ex b1 being non empty OrtStr st b1 is Oriented_Orthogonality_Space-like
proof end;
end;

definition
mode Oriented_Orthogonality_Space is non empty Oriented_Orthogonality_Space-like OrtStr ;
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
proof end;

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
proof end;

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 )
proof end;

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 ) )
proof 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 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;
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;

:: deftheorem 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;
attr IT is bach_transitive means :: 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 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;
attr IT is right_transitive means :: 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 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;
attr IT is left_transitive means :: 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 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;
attr IT is Euclidean_like means :: DIRORT:def 7
for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u1,u;
end;

:: deftheorem 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;
attr IT is Minkowskian_like means :: DIRORT:def 8
for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u,u1;
end;

:: deftheorem 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 )
proof end;

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 ;

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
proof end;

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 )
proof end;

theorem :: 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 )
proof end;

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
proof end;

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 )
proof end;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Euclidean_like for OrtStr ;
existence
ex b1 being Oriented_Orthogonality_Space st
( b1 is Euclidean_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive )
proof end;
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 )
proof end;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Minkowskian_like for OrtStr ;
existence
ex b1 being Oriented_Orthogonality_Space st
( b1 is Minkowskian_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive )
proof end;
end;

theorem Th15: :: DIRORT:15
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is right_transitive
proof end;

theorem :: DIRORT:16
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is bach_transitive
proof end;

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 )
proof end;

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
proof end;