:: DIRORT semantic presentation

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

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 AffinStruct ;
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 :

registration

cluster non empty Oriented_Orthogonality_Space-like AffinStruct ;
existence

proof end;

end;

definition

mode Oriented_Orthogonality_Space is non empty Oriented_Orthogonality_Space-like AffinStruct ;

end;

theorem :: DIRORT:3

canceled;

theorem Th4: :: DIRORT:4

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 Th5: :: DIRORT:5

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:6

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:7

canceled;

theorem :: DIRORT:8

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 :

definition

let AS be Oriented_Orthogonality_Space;
let a, b, c, d be Element of AS;
pred a,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 :

definition

let IT be Oriented_Orthogonality_Space;
attr IT 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 :

definition

let IT be Oriented_Orthogonality_Space;
attr IT 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 :

definition

let IT be Oriented_Orthogonality_Space;
attr IT 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 :

definition

let IT be Oriented_Orthogonality_Space;
attr IT 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 :

definition

let IT be Oriented_Orthogonality_Space;
attr IT 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 :

theorem :: DIRORT:9

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:10

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

proof end;

theorem :: DIRORT:11

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:12

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 Th13: :: DIRORT:13

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:14

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 Th15: :: DIRORT:15

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 bach_transitive right_transitive left_transitive Euclidean_like AffinStruct ;
existence

proof end;

end;

theorem Th16: :: DIRORT:16

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 bach_transitive right_transitive left_transitive Minkowskian_like AffinStruct ;
existence

proof end;

end;

theorem Th17: :: DIRORT:17

for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is right_transitive

proof end;

theorem :: DIRORT:18

for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is bach_transitive

proof end;

theorem :: DIRORT:19

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:20

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;