:: 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 b₁ being non empty OrtStr st b₁ 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 b₁ being Oriented_Orthogonality_Space st
( b₁ is Euclidean_like & b₁ is left_transitive & b₁ is right_transitive & b₁ 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 b₁ being Oriented_Orthogonality_Space st
( b₁ is Minkowskian_like & b₁ is left_transitive & b₁ is right_transitive & b₁ 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;