:: Fundamental Types of Metric Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 17, 1991
:: 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

cluster V44() OrtAfSp-like OrtAfPl-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ParOrtStr ;

existence
ex b₁ being OrtAfPl st
( b₁ is Euclidean & b₁ is Pappian & b₁ is Desarguesian & b₁ is Homogeneous & b₁ is translation & b₁ is Fanoian & b₁ is Moufangian )

proof end;

end;

registration

cluster V44() OrtAfSp-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ParOrtStr ;

existence
ex b₁ being OrtAfSp st
( b₁ is Euclidean & b₁ is Pappian & b₁ is Desarguesian & b₁ is Homogeneous & b₁ is translation & b₁ is Fanoian & b₁ 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;