:: DIRORT semantic presentation

notation

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄, c₅ be Element of c₁;
synonym c₂,c₃ '//' c₄,c₅ for c₂,c₃ // c₄,c₅;

end;

theorem Th1: :: DIRORT:1

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
( ( for b₄, b₅, b₆, b₇, b₈ being Element of (CESpace b₁,b₂,b₃) holds
( b₄,b₄ '//' b₆,b₈ & b₄,b₆ '//' b₈,b₈ & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₇,b₅ & not b₄ = b₆ implies b₅ = b₇ ) & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₅,b₈ & not b₄,b₆ '//' b₇,b₈ implies b₄,b₆ '//' b₈,b₇ ) & ( b₄,b₆ '//' b₅,b₇ implies b₆,b₄ '//' b₇,b₅ ) & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₇,b₈ implies b₄,b₆ '//' b₅,b₈ ) & ( not b₄,b₅ '//' b₆,b₇ or b₆,b₇ '//' b₄,b₅ or b₆,b₇ '//' b₅,b₄ ) ) ) & ( for b₄, b₅, b₆ being Element of (CESpace b₁,b₂,b₃) ex b₇ being Element of (CESpace b₁,b₂,b₃) st
( b₆ <> b₇ & b₆,b₇ '//' b₄,b₅ ) ) & ( for b₄, b₅, b₆ being Element of (CESpace b₁,b₂,b₃) ex b₇ being Element of (CESpace b₁,b₂,b₃) st
( b₆ <> b₇ & b₄,b₅ '//' b₆,b₇ ) ) )

proof end;

theorem Th2: :: DIRORT:2

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
( ( for b₄, b₅, b₆, b₇, b₈ being Element of (CMSpace b₁,b₂,b₃) holds
( b₄,b₄ '//' b₆,b₈ & b₄,b₆ '//' b₈,b₈ & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₇,b₅ & not b₄ = b₆ implies b₅ = b₇ ) & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₅,b₈ & not b₄,b₆ '//' b₇,b₈ implies b₄,b₆ '//' b₈,b₇ ) & ( b₄,b₆ '//' b₅,b₇ implies b₆,b₄ '//' b₇,b₅ ) & ( b₄,b₆ '//' b₅,b₇ & b₄,b₆ '//' b₇,b₈ implies b₄,b₆ '//' b₅,b₈ ) & ( not b₄,b₅ '//' b₆,b₇ or b₆,b₇ '//' b₄,b₅ or b₆,b₇ '//' b₅,b₄ ) ) ) & ( for b₄, b₅, b₆ being Element of (CMSpace b₁,b₂,b₃) ex b₇ being Element of (CMSpace b₁,b₂,b₃) st
( b₆ <> b₇ & b₆,b₇ '//' b₄,b₅ ) ) & ( for b₄, b₅, b₆ being Element of (CMSpace b₁,b₂,b₃) ex b₇ being Element of (CMSpace b₁,b₂,b₃) st
( b₆ <> b₇ & b₄,b₅ '//' b₆,b₇ ) ) )

proof end;

definition

let c₁ be non empty AffinStruct ;
attr a₁ is Oriented_Orthogonality_Space-like means :Def1: :: DIRORT:def 1
( ( for b₁, b₂, b₃, b₄, b₅ being Element of a₁ holds
( b₁,b₁ '//' b₃,b₅ & b₁,b₃ '//' b₅,b₅ & ( b₁,b₃ '//' b₂,b₄ & b₁,b₃ '//' b₄,b₂ & not b₁ = b₃ implies b₂ = b₄ ) & ( b₁,b₃ '//' b₂,b₄ & b₁,b₃ '//' b₂,b₅ & not b₁,b₃ '//' b₄,b₅ implies b₁,b₃ '//' b₅,b₄ ) & ( b₁,b₃ '//' b₂,b₄ implies b₃,b₁ '//' b₄,b₂ ) & ( b₁,b₃ '//' b₂,b₄ & b₁,b₃ '//' b₄,b₅ implies b₁,b₃ '//' b₂,b₅ ) & ( not b₁,b₂ '//' b₃,b₄ or b₃,b₄ '//' b₁,b₂ or b₃,b₄ '//' b₂,b₁ ) ) ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( b₃ <> b₄ & b₃,b₄ '//' b₁,b₂ ) ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( b₃ <> b₄ & b₁,b₂ '//' b₃,b₄ ) ) );

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 Th3: :: DIRORT:3

canceled;

theorem Th4: :: DIRORT:4

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
CMSpace b₁,b₂,b₃ is Oriented_Orthogonality_Space

proof end;

theorem Th5: :: DIRORT:5

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
CESpace b₁,b₂,b₃ is Oriented_Orthogonality_Space

proof end;

theorem Th6: :: DIRORT:6

for b₁ being Oriented_Orthogonality_Space
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₅,b₄ '//' b₂,b₃ & b₅ <> b₄ )

proof end;

theorem Th7: :: DIRORT:7

canceled;

theorem Th8: :: DIRORT:8

for b₁ being Oriented_Orthogonality_Space
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂ <> b₅ & ( b₃,b₄ '//' b₂,b₅ or b₃,b₄ '//' b₅,b₂ ) )

proof end;

definition

let c₁ be Oriented_Orthogonality_Space;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ _|_ c₄,c₅ means :: DIRORT:def 2
( a₂,a₃ '//' a₄,a₅ or a₂,a₃ '//' a₅,a₄ );

end;

:: deftheorem Def2 defines _|_ DIRORT:def 2 :

definition

let c₁ be Oriented_Orthogonality_Space;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ // c₄,c₅ means :Def3: :: DIRORT:def 3
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & b₁,b₂ '//' a₂,a₃ & b₁,b₂ '//' a₄,a₅ );

end;

:: deftheorem Def3 defines // DIRORT:def 3 :

definition

let c₁ be Oriented_Orthogonality_Space;
attr a₁ is bach_transitive means :Def4: :: DIRORT:def 4
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁,b₂ '//' b₄,b₅ & b₇,b₈ '//' b₄,b₅ & b₇,b₈ '//' b₃,b₆ & not b₇ = b₈ & not b₄ = b₅ holds
b₁,b₂ '//' b₃,b₆;

end;

:: deftheorem Def4 defines bach_transitive DIRORT:def 4 :

definition

let c₁ be Oriented_Orthogonality_Space;
attr a₁ is right_transitive means :Def5: :: DIRORT:def 5
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁,b₂ '//' b₄,b₅ & b₄,b₅ '//' b₇,b₈ & b₃,b₆ '//' b₇,b₈ & not b₇ = b₈ & not b₄ = b₅ holds
b₁,b₂ '//' b₃,b₆;

end;

:: deftheorem Def5 defines right_transitive DIRORT:def 5 :

definition

let c₁ be Oriented_Orthogonality_Space;
attr a₁ is left_transitive means :Def6: :: DIRORT:def 6
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁,b₂ '//' b₄,b₅ & b₄,b₅ '//' b₇,b₈ & b₁,b₂ '//' b₃,b₆ & not b₁ = b₂ & not b₄ = b₅ holds
b₃,b₆ '//' b₇,b₈;

end;

:: deftheorem Def6 defines left_transitive DIRORT:def 6 :

definition

let c₁ be Oriented_Orthogonality_Space;
attr a₁ is Euclidean_like means :Def7: :: DIRORT:def 7
for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ '//' b₃,b₄ holds
b₃,b₄ '//' b₂,b₁;

end;

:: deftheorem Def7 defines Euclidean_like DIRORT:def 7 :

definition

let c₁ be Oriented_Orthogonality_Space;
attr a₁ is Minkowskian_like means :Def8: :: DIRORT:def 8
for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ '//' b₃,b₄ holds
b₃,b₄ '//' b₁,b₂;

end;

:: deftheorem Def8 defines Minkowskian_like DIRORT:def 8 :

theorem Th9: :: DIRORT:9

for b₁ being Oriented_Orthogonality_Space
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ // b₄,b₄ & b₄,b₄ // b₂,b₃ )

proof end;

theorem Th10: :: DIRORT:10

for b₁ being Oriented_Orthogonality_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

theorem Th11: :: DIRORT:11

for b₁ being Oriented_Orthogonality_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₃,b₂ // b₅,b₄

proof end;

theorem Th12: :: DIRORT:12

for b₁ being Oriented_Orthogonality_Space holds
( b₁ is left_transitive iff for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ // b₆,b₇ & b₂,b₃ '//' b₄,b₅ & b₂ <> b₃ holds
b₆,b₇ '//' b₄,b₅ )

proof end;

theorem Th13: :: DIRORT:13

for b₁ being Oriented_Orthogonality_Space holds
( b₁ is bach_transitive iff for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ '//' b₅,b₆ & b₅,b₆ // b₄,b₇ & b₅ <> b₆ holds
b₂,b₃ '//' b₄,b₇ )

proof end;

theorem Th14: :: DIRORT:14

for b₁ being Oriented_Orthogonality_Space st b₁ is bach_transitive holds
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₄,b₅ // b₆,b₇ & b₄ <> b₅ holds
b₂,b₃ // b₆,b₇

proof end;

theorem Th15: :: DIRORT:15

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Oriented_Orthogonality_Space st Gen b₂,b₃ & b₄ = CESpace b₁,b₂,b₃ holds
( b₄ is Euclidean_like & b₄ is left_transitive & b₄ is right_transitive & b₄ 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 b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Oriented_Orthogonality_Space st Gen b₂,b₃ & b₄ = CMSpace b₁,b₂,b₃ holds
( b₄ is Minkowskian_like & b₄ is left_transitive & b₄ is right_transitive & b₄ 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 b₁ being Oriented_Orthogonality_Space st b₁ is left_transitive holds
b₁ is right_transitive

proof end;

theorem Th18: :: DIRORT:18

for b₁ being Oriented_Orthogonality_Space st b₁ is left_transitive holds
b₁ is bach_transitive

proof end;

theorem Th19: :: DIRORT:19

for b₁ being Oriented_Orthogonality_Space st b₁ is bach_transitive holds
( b₁ is right_transitive iff for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ '//' b₆,b₇ & b₄,b₅ '//' b₆,b₇ & b₆ <> b₇ holds
b₂,b₃ // b₄,b₅ )

proof end;

theorem Th20: :: DIRORT:20

for b₁ being Oriented_Orthogonality_Space st b₁ is right_transitive & ( b₁ is Euclidean_like or b₁ is Minkowskian_like ) holds
b₁ is left_transitive

proof end;