begin
:: deftheorem Def1 defines Euclidean EUCLMETR:def 1 :
:: deftheorem Def2 defines Pappian EUCLMETR:def 2 :
:: deftheorem Def3 defines Desarguesian EUCLMETR:def 3 :
:: deftheorem Def4 defines Fanoian EUCLMETR:def 4 :
:: deftheorem Def5 defines Moufangian EUCLMETR:def 5 :
:: deftheorem Def6 defines translation EUCLMETR:def 6 :
definition
let IT be
OrtAfSp;
attr IT is
Homogeneous means :
Def7:
for
o,
a,
a1,
b,
b1,
c,
c1 being
Element of
IT st
o,
a _|_ o,
a1 &
o,
b _|_ o,
b1 &
o,
c _|_ o,
c1 &
a,
b _|_ a1,
b1 &
a,
c _|_ a1,
c1 & not
o,
c // o,
a & not
o,
a // o,
b holds
b,
c _|_ b1,
c1;
end;
:: deftheorem Def7 defines Homogeneous EUCLMETR:def 7 :
for
IT being
OrtAfSp holds
(
IT is
Homogeneous iff for
o,
a,
a1,
b,
b1,
c,
c1 being
Element of
IT st
o,
a _|_ o,
a1 &
o,
b _|_ o,
b1 &
o,
c _|_ o,
c1 &
a,
b _|_ a1,
b1 &
a,
c _|_ a1,
c1 & not
o,
c // o,
a & not
o,
a // o,
b holds
b,
c _|_ b1,
c1 );
theorem Th1:
theorem Th2:
theorem
theorem Th4:
for
MP being
OrtAfSp for
x,
y,
z being
Element of
MP st
LIN x,
y,
z holds
(
LIN x,
z,
y &
LIN y,
x,
z &
LIN y,
z,
x &
LIN z,
x,
y &
LIN z,
y,
x )
theorem Th5:
theorem Th6:
for
MS being
OrtAfPl for
a,
b,
c,
d1,
d2 being
Element of
MS st not
LIN a,
b,
c &
d1,
a _|_ b,
c &
d1,
b _|_ a,
c &
d2,
a _|_ b,
c &
d2,
b _|_ a,
c holds
d1 = d2
theorem Th7:
for
MS being
OrtAfPl for
a,
b,
c,
d being
Element of
MS st
a,
b _|_ c,
d &
b,
c _|_ a,
d &
LIN a,
b,
c & not
a = c & not
a = b holds
b = c
theorem Th8:
theorem Th9:
Lm1:
for MS being OrtAfPl holds
( MS is satisfying_PAP iff Af MS is Pappian )
theorem Th10:
Lm2:
for MS being OrtAfPl holds
( MS is satisfying_DES iff Af MS is Desarguesian )
theorem Th11:
theorem
Lm3:
for MS being OrtAfPl holds
( MS is satisfying_des iff Af MS is translational )
theorem
theorem Th14:
theorem Th15:
theorem Th16:
for
MS being
OrtAfPl for
o,
c,
c1,
a,
a1,
a2 being
Element of
MS st not
LIN o,
c,
a &
o <> c1 &
o,
c _|_ o,
c1 &
o,
a _|_ o,
a1 &
o,
a _|_ o,
a2 &
c,
a _|_ c1,
a1 &
c,
a _|_ c1,
a2 holds
a1 = a2
theorem
Lm4:
for V being RealLinearSpace
for u, v, y being VECTOR of V holds
( (u - y) - (v - y) = u - v & (u + y) - (v + y) = u - v )
Lm5:
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c being Real holds
( PProJ w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y)) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
theorem Th18:
theorem Th19:
for
V being
RealLinearSpace for
w,
y,
u,
v being
VECTOR of
V st
Gen w,
y &
0. V <> u &
0. V <> v &
u,
v are_Ort_wrt w,
y holds
ex
c being
Real st
for
a,
b being
Real holds
(
(a * w) + (b * y),
((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,
y &
((a * w) + (b * y)) - u,
(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,
y )
Lm6:
for V being RealLinearSpace
for w, y being VECTOR of V
for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
Lm7:
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
theorem
canceled;
theorem Th21:
theorem Th22:
for
MS being
OrtAfPl for
o,
a,
a1,
b,
b1,
c,
c1 being
Element of
MS st
o,
b _|_ o,
b1 &
o,
c _|_ o,
c1 &
a,
b _|_ a1,
b1 &
a,
c _|_ a1,
c1 & not
o,
c // o,
a & not
o,
a // o,
b &
o = a1 holds
b,
c _|_ b1,
c1
theorem Th23:
theorem