:: Fanoian, Pappian and Desarguesian Affine Spaces
:: by Krzysztof Pra\.zmowski
::
:: Received November 16, 1990
:: 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;

cluster Lambda OAS -> 2-dimensional ;

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 (OASpace V) 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 Th6, Th11;

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 Th9, Th11;

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

cluster V54() non trivial OAffinSpace-like Pappian Desarguesian Moufangian translation for AffinStruct ;

existence
ex b₁ being OAffinSpace st
( b₁ is Pappian & b₁ is Desarguesian & b₁ is Moufangian & b₁ is translation )

proof end;

end;

registration

cluster V54() non trivial strict AffinSpace-like 2-dimensional Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;

existence
ex b₁ being AffinPlane st
( b₁ is strict & b₁ is Fanoian & b₁ is Pappian & b₁ is Desarguesian & b₁ is Moufangian & b₁ is translational )

proof end;

end;

registration

cluster V54() non trivial strict AffinSpace-like Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;

existence
ex b₁ being AffinSpace st
( b₁ is strict & b₁ is Fanoian & b₁ is Pappian & b₁ is Desarguesian & b₁ is Moufangian & b₁ 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;

cluster Lambda OAS -> Desarguesian ;

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;

cluster Lambda OAS -> translational ;

correctness
coherence
Lambda OAS is translational ;
by Def5;

end;