begin
theorem Th1:
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
( ( for
u,
u1,
v,
v1,
w being
Element of 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 ex
u1 being
Element of st
(
w <> u1 &
w,
u1 '//' u,
v ) ) & ( for
u,
v,
w being
Element of ex
u1 being
Element of st
(
w <> u1 &
u,
v '//' w,
u1 ) ) )
theorem Th2:
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
( ( for
u,
u1,
v,
v1,
w being
Element of 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 ex
u1 being
Element of st
(
w <> u1 &
w,
u1 '//' u,
v ) ) & ( for
u,
v,
w being
Element of ex
u1 being
Element of st
(
w <> u1 &
u,
v '//' w,
u1 ) ) )
definition
let IT be non
empty AffinStruct ;
attr IT is
Oriented_Orthogonality_Space-like means :
Def1:
( ( for
u,
u1,
v,
v1,
w being
Element of 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 ex
u1 being
Element of st
(
w <> u1 &
w,
u1 '//' u,
v ) ) & ( for
u,
v,
w being
Element of ex
u1 being
Element of 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 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 ex
u1 being
Element of st
(
w <> u1 &
w,
u1 '//' u,
v ) ) & ( for
u,
v,
w being
Element of ex
u1 being
Element of st
(
w <> u1 &
u,
v '//' w,
u1 ) ) ) );
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem
canceled;
theorem
:: deftheorem defines _|_ DIRORT:def 2 :
definition
let AS be
Oriented_Orthogonality_Space;
let a,
b,
c,
d be
Element of ;
pred a,
b // c,
d means :
Def3:
ex
e,
f being
Element of 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 holds
(
a,
b // c,
d iff ex
e,
f being
Element of 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:
for
u,
u1,
u2,
v,
v1,
v2,
w,
w1 being
Element of 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 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:
for
u,
u1,
u2,
v,
v1,
v2,
w,
w1 being
Element of 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 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:
for
u,
u1,
u2,
v,
v1,
v2,
w,
w1 being
Element of 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 st
u,
u1 '//' v,
v1 &
v,
v1 '//' w,
w1 &
u,
u1 '//' u2,
v2 & not
u = u1 & not
v = v1 holds
u2,
v2 '//' w,
w1 );
:: deftheorem Def7 defines Euclidean_like DIRORT:def 7 :
:: deftheorem Def8 defines Minkowskian_like DIRORT:def 8 :
theorem
theorem
theorem
theorem
for
AS being
Oriented_Orthogonality_Space holds
(
AS is
left_transitive iff for
v,
v1,
w,
w1,
u2,
v2 being
Element of st
v,
v1 // u2,
v2 &
v,
v1 '//' w,
w1 &
v <> v1 holds
u2,
v2 '//' w,
w1 )
theorem Th13:
for
AS being
Oriented_Orthogonality_Space holds
(
AS is
bach_transitive iff for
u,
u1,
u2,
v,
v1,
v2 being
Element of st
u,
u1 '//' v,
v1 &
v,
v1 // u2,
v2 &
v <> v1 holds
u,
u1 '//' u2,
v2 )
theorem
for
AS being
Oriented_Orthogonality_Space st
AS is
bach_transitive holds
for
u,
u1,
v,
v1,
w,
w1 being
Element of st
u,
u1 // v,
v1 &
v,
v1 // w,
w1 &
v <> v1 holds
u,
u1 // w,
w1
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem
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 st
u,
u1 '//' u2,
v2 &
v,
v1 '//' u2,
v2 &
u2 <> v2 holds
u,
u1 // v,
v1 )
theorem