:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received April 17, 1991

:: Copyright (c) 1991-2018 Association of Mizar Users

:: 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 );

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;

end;
attr IT is Pappian means :Def2: :: EUCLMETR:def 2

AffinStruct(# the carrier of IT, the CONGR of IT #) is Pappian ;

AffinStruct(# the carrier of IT, the CONGR of IT #) is Pappian ;

:: 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 );

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;

end;
attr IT is Desarguesian means :Def3: :: EUCLMETR:def 3

AffinStruct(# the carrier of IT, the CONGR of IT #) is Desarguesian ;

AffinStruct(# the carrier of IT, the CONGR of IT #) is Desarguesian ;

:: 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 );

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;

end;
attr IT is Fanoian means :Def4: :: EUCLMETR:def 4

AffinStruct(# the carrier of IT, the CONGR of IT #) is Fanoian ;

AffinStruct(# the carrier of IT, the CONGR of IT #) is Fanoian ;

:: 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 );

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;

end;
attr IT is Moufangian means :Def5: :: EUCLMETR:def 5

AffinStruct(# the carrier of IT, the CONGR of IT #) is Moufangian ;

AffinStruct(# the carrier of IT, the CONGR of IT #) is Moufangian ;

:: 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 );

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;

end;
attr IT is translation means :Def6: :: EUCLMETR:def 6

AffinStruct(# the carrier of IT, the CONGR of IT #) is translational ;

AffinStruct(# the carrier of IT, the CONGR of IT #) is translational ;

:: 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 );

for IT being OrtAfSp holds

( IT is translation iff AffinStruct(# the carrier of IT, the CONGR of IT #) is translational );

:: 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 );

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 )

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 )

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

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 )

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 )

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

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

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;

Lm1: for MS being OrtAfPl holds

( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )

proof end;

Lm2: for MS being OrtAfPl holds

( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )

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

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

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 )

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) )

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 )

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

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

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

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

ex b_{1} being OrtAfPl st

( b_{1} is Euclidean & b_{1} is Pappian & b_{1} is Desarguesian & b_{1} is Homogeneous & b_{1} is translation & b_{1} is Fanoian & b_{1} is Moufangian )
end;

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

existence ex b

( b

proof end;

registration

ex b_{1} being OrtAfSp st

( b_{1} is Euclidean & b_{1} is Pappian & b_{1} is Desarguesian & b_{1} is Homogeneous & b_{1} is translation & b_{1} is Fanoian & b_{1} is Moufangian )
end;

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

existence ex b

( b

proof 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

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;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

by Def2;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

by Def2;

registration

let MS be Desarguesian OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

by Def3;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

by Def3;

registration

let MS be Moufangian OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian ;

by Def5;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian ;

by Def5;

registration

let MS be translation OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ;

by Def6;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ;

by Def6;

registration

let MS be Fanoian OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian ;

by Def4;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian ;

by Def4;

registration

let MS be Homogeneous OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

proof end;

registration

let MS be Euclidean Desarguesian OrtAfPl;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

proof end;

registration

let MS be Pappian OrtAfSp;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

by Def2;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ;

by Def2;

registration

let MS be Desarguesian OrtAfSp;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

by Def3;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ;

by Def3;

registration

let MS be Moufangian OrtAfSp;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian ;

by Def5;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian ;

by Def5;

registration

let MS be translation OrtAfSp;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ;

by Def6;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ;

by Def6;

registration

let MS be Fanoian OrtAfSp;

correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian ;

by Def4;

end;
correctness

coherence

AffinStruct(# the carrier of MS, the CONGR of MS #) is Fanoian ;

by Def4;