:: Fundamental Types of Metric Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1991-2021 Association of Mizar Users

definition
let IT be OrtAfSp;
attr IT is Euclidean means :: EUCLMETR:def 1
for a, b, c, d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c;
end;

:: deftheorem defines Euclidean EUCLMETR:def 1 :
for IT being OrtAfSp holds
( IT is Euclidean iff for a, b, c, d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c );

definition
let IT be OrtAfSp;
attr IT is Pappian means :Def2: :: EUCLMETR:def 2
AffinStruct(# the carrier of IT, the CONGR of IT #) is Pappian ;
end;

:: deftheorem Def2 defines Pappian EUCLMETR:def 2 :
for IT being OrtAfSp holds
( IT is Pappian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Pappian );

definition
let IT be OrtAfSp;
attr IT is Desarguesian means :Def3: :: EUCLMETR:def 3
AffinStruct(# the carrier of IT, the CONGR of IT #) is Desarguesian ;
end;

:: deftheorem Def3 defines Desarguesian EUCLMETR:def 3 :
for IT being OrtAfSp holds
( IT is Desarguesian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Desarguesian );

definition
let IT be OrtAfSp;
attr IT is Fanoian means :Def4: :: EUCLMETR:def 4
AffinStruct(# the carrier of IT, the CONGR of IT #) is Fanoian ;
end;

:: deftheorem Def4 defines Fanoian EUCLMETR:def 4 :
for IT being OrtAfSp holds
( IT is Fanoian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Fanoian );

definition
let IT be OrtAfSp;
attr IT is Moufangian means :Def5: :: EUCLMETR:def 5
AffinStruct(# the carrier of IT, the CONGR of IT #) is Moufangian ;
end;

:: deftheorem Def5 defines Moufangian EUCLMETR:def 5 :
for IT being OrtAfSp holds
( IT is Moufangian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Moufangian );

definition
let IT be OrtAfSp;
attr IT is translation means :Def6: :: EUCLMETR:def 6
AffinStruct(# the carrier of IT, the CONGR of IT #) is translational ;
end;

:: deftheorem Def6 defines translation EUCLMETR:def 6 :
for IT being OrtAfSp holds
( IT is translation iff AffinStruct(# the carrier of IT, the CONGR of IT #) is translational );

definition
let IT be OrtAfSp;
attr IT is Homogeneous means :: EUCLMETR:def 7
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 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: :: EUCLMETR:1
for MP being OrtAfSp
for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
proof end;

theorem Th2: :: EUCLMETR:2
for MS being OrtAfPl
for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
proof end;

theorem :: EUCLMETR:3
for MS being OrtAfPl
for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
proof end;

theorem Th4: :: EUCLMETR:4
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 )
proof end;

theorem Th5: :: EUCLMETR:5
for MS being OrtAfPl
for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
proof end;

theorem Th6: :: EUCLMETR:6
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
proof end;

theorem Th7: :: EUCLMETR:7
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
proof end;

theorem Th8: :: EUCLMETR:8
for MS being OrtAfPl holds
( MS is Euclidean iff MS is satisfying_3H )
proof end;

theorem Th9: :: EUCLMETR:9
for MS being OrtAfPl holds
( MS is Homogeneous iff MS is satisfying_ODES ) by CONAFFM:def 4;

Lm1: for MS being OrtAfPl holds
( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )

proof end;

theorem Th10: :: EUCLMETR:10
for MS being OrtAfPl holds
( MS is Pappian iff MS is satisfying_PAP ) by Lm1;

Lm2: for MS being OrtAfPl holds
( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )

proof end;

theorem Th11: :: EUCLMETR:11
for MS being OrtAfPl holds
( MS is Desarguesian iff MS is satisfying_DES ) by Lm2;

theorem :: EUCLMETR:12
for MS being OrtAfPl holds
( MS is Moufangian iff MS is satisfying_TDES )
proof end;

Lm3: for MS being OrtAfPl holds
( MS is satisfying_des iff AffinStruct(# the carrier of MS, the CONGR of MS #) is translational )

proof end;

theorem :: EUCLMETR:13
for MS being OrtAfPl holds
( MS is translation iff MS is satisfying_des ) by Lm3;

theorem Th14: :: EUCLMETR:14
for MS being OrtAfPl st MS is Homogeneous holds
MS is Desarguesian
proof end;

theorem Th15: :: EUCLMETR:15
for MS being OrtAfPl st MS is Euclidean & MS is Desarguesian holds
MS is Pappian
proof end;

theorem Th16: :: EUCLMETR:16
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
proof end;

theorem :: EUCLMETR:17
for MS being OrtAfPl
for o, c, c1, a being Element of MS st not LIN o,c,a holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
proof end;

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 )

proof end;

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 )

proof end;

theorem Th18: :: EUCLMETR:18
for V being RealLinearSpace
for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
proof end;

theorem Th19: :: EUCLMETR:19
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 )
proof end;

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)

proof end;

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 )

proof end;

theorem Th20: :: EUCLMETR:20
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is satisfying_LIN
proof end;

theorem Th21: :: EUCLMETR:21
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
proof end;

theorem Th22: :: EUCLMETR:22
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Homogeneous
proof end;

registration
existence
ex b1 being OrtAfPl st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof end;
end;

registration
existence
ex b1 being OrtAfSp st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof end;
end;

theorem :: EUCLMETR:23
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
proof end;

registration
let MS be Pappian OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Pappian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian
;
by Def2;
end;

registration
let MS be Desarguesian OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Desarguesian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian
;
by Def3;
end;

registration
let MS be Moufangian OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Moufangian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian
;
by Def5;
end;

registration
let MS be translation OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> translational ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is translational
;
by Def6;
end;

registration
let MS be Fanoian OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Fanoian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian
;
by Def4;
end;

registration
let MS be Homogeneous OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Desarguesian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian
;
proof end;
end;

registration
let MS be Euclidean Desarguesian OrtAfPl;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Pappian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian
;
proof end;
end;

registration
let MS be Pappian OrtAfSp;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Pappian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian
;
by Def2;
end;

registration
let MS be Desarguesian OrtAfSp;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Desarguesian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian
;
by Def3;
end;

registration
let MS be Moufangian OrtAfSp;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Moufangian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian
;
by Def5;
end;

registration
let MS be translation OrtAfSp;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> translational ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is translational
;
by Def6;
end;

registration
let MS be Fanoian OrtAfSp;
cluster AffinStruct(# the carrier of MS, the CONGR of MS #) -> Fanoian ;
correctness
coherence
AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian
;
by Def4;
end;