:: DIRORT semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 AffinStruct ;
existence
ex b1 being non empty AffinStruct st b1 is Oriented_Orthogonality_Space-like
proof end;
end;

definition
mode Oriented_Orthogonality_Space is non empty Oriented_Orthogonality_Space-like AffinStruct ;
end;

theorem :: DIRORT:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: DIRORT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRORT:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :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;
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 :
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 :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;
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 :
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 :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;
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 :
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:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 Th16: :: DIRORT:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 Th17: :: DIRORT:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is right_transitive
proof end;

theorem :: DIRORT:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is bach_transitive
proof end;

theorem :: DIRORT:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;