:: Fanoian, Pappian and Desarguesian Affine Spaces
:: by Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

registration
let OAS be OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like ;
correctness
coherence
( Lambda OAS is AffinSpace-like & not Lambda OAS is trivial )
;
by DIRAF:41;
end;

registration
let OAS be OAffinPlane;
correctness
coherence
Lambda OAS is 2-dimensional
;
by DIRAF:45;
end;

theorem Th1: :: PAPDESAF:1
for OAS being OAffinSpace
for x being set holds
( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )
proof end;

theorem Th2: :: PAPDESAF:2
for OAS being OAffinSpace
for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( a,b,c are_collinear iff LIN a9,b9,c9 )
proof end;

theorem Th3: :: PAPDESAF:3
for V being RealLinearSpace
for x being set holds
( x is Element of () iff x is VECTOR of V )
proof end;

theorem Th4: :: PAPDESAF:4
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
proof end;

theorem :: PAPDESAF:5
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
proof end;

definition
let AS be AffinSpace;
redefine attr AS is Fanoian means :: PAPDESAF:def 1
for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c;
compatibility
( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c )
proof end;
end;

:: deftheorem defines Fanoian PAPDESAF:def 1 :
for AS being AffinSpace holds
( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c );

definition
let IT be OAffinSpace;
attr IT is Pappian means :Def2: :: PAPDESAF:def 2
Lambda IT is Pappian ;
attr IT is Desarguesian means :Def3: :: PAPDESAF:def 3
Lambda IT is Desarguesian ;
attr IT is Moufangian means :Def4: :: PAPDESAF:def 4
Lambda IT is Moufangian ;
attr IT is translation means :Def5: :: PAPDESAF:def 5
Lambda IT is translational ;
end;

:: deftheorem Def2 defines Pappian PAPDESAF:def 2 :
for IT being OAffinSpace holds
( IT is Pappian iff Lambda IT is Pappian );

:: deftheorem Def3 defines Desarguesian PAPDESAF:def 3 :
for IT being OAffinSpace holds
( IT is Desarguesian iff Lambda IT is Desarguesian );

:: deftheorem Def4 defines Moufangian PAPDESAF:def 4 :
for IT being OAffinSpace holds
( IT is Moufangian iff Lambda IT is Moufangian );

:: deftheorem Def5 defines translation PAPDESAF:def 5 :
for IT being OAffinSpace holds
( IT is translation iff Lambda IT is translational );

definition
let OAS be OAffinSpace;
attr OAS is satisfying_DES means :: PAPDESAF:def 6
for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
end;

:: deftheorem defines satisfying_DES PAPDESAF:def 6 :
for OAS being OAffinSpace holds
( OAS is satisfying_DES iff for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );

definition
let OAS be OAffinSpace;
attr OAS is satisfying_DES_1 means :: PAPDESAF:def 7
for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1;
end;

:: deftheorem defines satisfying_DES_1 PAPDESAF:def 7 :
for OAS being OAffinSpace holds
( OAS is satisfying_DES_1 iff for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1 );

theorem Th6: :: PAPDESAF:6
for OAS being OAffinSpace st OAS is satisfying_DES_1 holds
OAS is satisfying_DES
proof end;

theorem Th7: :: PAPDESAF:7
for OAS being OAffinSpace
for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & a,o // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds
( b,o // o,b9 & a,b // b9,a9 )
proof end;

theorem Th8: :: PAPDESAF:8
for OAS being OAffinSpace
for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )
proof end;

theorem Th9: :: PAPDESAF:9
for OAP being OAffinSpace st OAP is satisfying_DES_1 holds
Lambda OAP is Desarguesian
proof end;

theorem Th10: :: PAPDESAF:10
for V being RealLinearSpace
for o, u, v, u1, v1 being VECTOR of V
for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
proof end;

Lm1: for V being RealLinearSpace
for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds
ex r being Real st
( v - u = r * (w - v) & 0 < r )

proof end;

theorem Th11: :: PAPDESAF:11
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
OAS is satisfying_DES_1
proof end;

theorem :: PAPDESAF:12
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
( OAS is satisfying_DES_1 & OAS is satisfying_DES ) by ;

Lm2: for V being RealLinearSpace
for y, u, v being VECTOR of V st y,u '||' y,v & y <> u & y <> v holds
ex r being Real st
( u - y = r * (v - y) & r <> 0 )

proof end;

Lm3: for V being RealLinearSpace
for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v

proof end;

theorem Th13: :: PAPDESAF:13
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Pappian
proof end;

theorem Th14: :: PAPDESAF:14
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Desarguesian by ;

theorem Th15: :: PAPDESAF:15
for AS being AffinSpace st AS is Desarguesian holds
AS is Moufangian
proof end;

theorem Th16: :: PAPDESAF:16
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Moufangian
proof end;

theorem Th17: :: PAPDESAF:17
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is translational
proof end;

theorem Th18: :: PAPDESAF:18
for OAS being OAffinSpace holds Lambda OAS is Fanoian
proof end;

registration
existence
ex b1 being OAffinSpace st
( b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translation )
proof end;
end;

registration
existence
ex b1 being AffinPlane st
( b1 is strict & b1 is Fanoian & b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translational )
proof end;
end;

registration
existence
ex b1 being AffinSpace st
( b1 is strict & b1 is Fanoian & b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translational )
proof end;
end;

registration
let OAS be OAffinSpace;
cluster Lambda OAS -> Fanoian ;
correctness
coherence
Lambda OAS is Fanoian
;
by Th18;
end;

registration
let OAS be Pappian OAffinSpace;
cluster Lambda OAS -> Pappian ;
correctness
coherence
Lambda OAS is Pappian
;
by Def2;
end;

registration
let OAS be Desarguesian OAffinSpace;
correctness
coherence
Lambda OAS is Desarguesian
;
by Def3;
end;

registration
let OAS be Moufangian OAffinSpace;
cluster Lambda OAS -> Moufangian ;
correctness
coherence
Lambda OAS is Moufangian
;
by Def4;
end;

registration
let OAS be translation OAffinSpace;
correctness
coherence
Lambda OAS is translational
;
by Def5;
end;