:: PAPDESAF semantic presentation

registration

let OAS be OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like ;
correctness by DIRAF:48;

end;

registration

let OAS be OAffinPlane;
cluster Lambda OAS -> non trivial AffinSpace-like 2-dimensional ;
correctness by DIRAF:53;

end;

theorem :: PAPDESAF:1

canceled;

theorem Th2: :: PAPDESAF:2

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 Th3: :: PAPDESAF:3

for OAS being OAffinSpace
for a, b, c being Element of OAS
for a', b', c' being Element of (Lambda OAS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )

proof end;

theorem Th4: :: PAPDESAF:4

for V being RealLinearSpace
for x being set holds
( x is Element of (OASpace V) iff x is VECTOR of V )

proof end;

theorem Th5: :: PAPDESAF:5

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:6

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;

notation

let AS be AffinSpace;
synonym AS satisfies_PAP' for Pappian ASAS satisfies_PAP ;

end;

notation

let AS be AffinSpace;
synonym AS satisfies_DES' for Desarguesian ASAS satisfies_DES ;

end;

notation

let AS be AffinSpace;
synonym AS satisfies_TDES' for Moufangian ASAS satisfies_TDES ;

end;

notation

let AS be AffinSpace;
synonym AS satisfies_des' for translational ASAS satisfies_des ;

end;

notation

let AS be AffinSpace;
synonym AS satisfies_Fano for Fanoian ASAS satisfies_Fano ;

end;

definition

let AS be AffinSpace;
canceled;
canceled;
canceled;
canceled;
redefine attr AS is Fanoian means :Def5: :: PAPDESAF:def 5
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

proof end;

end;

:: deftheorem PAPDESAF:def 1 :

:: deftheorem PAPDESAF:def 2 :

:: deftheorem PAPDESAF:def 3 :

:: deftheorem PAPDESAF:def 4 :

:: deftheorem Def5 defines satisfies_Fano PAPDESAF:def 5 :

definition

let IT be OAffinSpace;
canceled;
canceled;
canceled;
canceled;
canceled;
attr IT is Pappian means :Def11: :: PAPDESAF:def 11
Lambda IT satisfies_PAP' ;
attr IT is Desarguesian means :Def12: :: PAPDESAF:def 12
Lambda IT satisfies_DES' ;
attr IT is Moufangian means :Def13: :: PAPDESAF:def 13
Lambda IT satisfies_TDES' ;
attr IT is translation means :Def14: :: PAPDESAF:def 14
Lambda IT satisfies_des' ;

end;

:: deftheorem PAPDESAF:def 6 :

:: deftheorem PAPDESAF:def 7 :

:: deftheorem PAPDESAF:def 8 :

:: deftheorem PAPDESAF:def 9 :

:: deftheorem PAPDESAF:def 10 :

:: deftheorem Def11 defines Pappian PAPDESAF:def 11 :

:: deftheorem Def12 defines Desarguesian PAPDESAF:def 12 :

:: deftheorem Def13 defines Moufangian PAPDESAF:def 13 :

:: deftheorem Def14 defines translation PAPDESAF:def 14 :

definition

let OAS be OAffinSpace;
attr OAS is satisfying_DES means :Def15: :: PAPDESAF:def 15
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 LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;

end;

:: deftheorem Def15 defines satisfying_DES PAPDESAF:def 15 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_DES for satisfying_DES OAS;

end;

definition

let OAS be OAffinSpace;
attr OAS is satisfying_DES_1 means :Def16: :: PAPDESAF:def 16
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 LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1;

end;

:: deftheorem Def16 defines satisfying_DES_1 PAPDESAF:def 16 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_DES_1 for satisfying_DES_1 OAS;

end;

theorem :: PAPDESAF:7

canceled;

theorem :: PAPDESAF:8

canceled;

theorem :: PAPDESAF:9

canceled;

theorem :: PAPDESAF:10

canceled;

theorem Th11: :: PAPDESAF:11

for OAS being OAffinSpace st OAS satisfies_DES_1 holds
OAS satisfies_DES

proof end;

theorem Th12: :: PAPDESAF:12

for OAS being OAffinSpace
for o, a, b, a', b' being Element of the carrier of OAS st not LIN o,a,b & a,o // o,a' & LIN o,b,b' & a,b '||' a',b' holds
( b,o // o,b' & a,b // b',a' )

proof end;

theorem Th13: :: PAPDESAF:13

for OAS being OAffinSpace
for o, a, b, a', b' being Element of the carrier of OAS st not LIN o,a,b & o,a // o,a' & LIN o,b,b' & a,b '||' a',b' holds
( o,b // o,b' & a,b // a',b' )

proof end;

theorem Th14: :: PAPDESAF:14

for OAP being OAffinSpace st OAP satisfies_DES_1 holds
Lambda OAP satisfies_DES'

proof end;

theorem Th15: :: PAPDESAF:15

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 :: PAPDESAF:16

canceled;

theorem Th17: :: PAPDESAF:17

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
OAS satisfies_DES_1

proof end;

theorem Th18: :: PAPDESAF:18

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
( OAS satisfies_DES_1 & OAS satisfies_DES )

proof end;

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 Th19: :: PAPDESAF:19

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS satisfies_PAP'

proof end;

theorem Th20: :: PAPDESAF:20

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS satisfies_DES'

proof end;

theorem Th21: :: PAPDESAF:21

for AS being AffinSpace st AS satisfies_DES' holds
AS satisfies_TDES'

proof end;

theorem Th22: :: PAPDESAF:22

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS satisfies_TDES'

proof end;

theorem Th23: :: PAPDESAF:23

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS satisfies_des'

proof end;

theorem Th24: :: PAPDESAF:24

for OAS being OAffinSpace holds Lambda OAS satisfies_Fano

proof end;

registration

cluster Pappian Desarguesian Moufangian translation AffinStruct ;
existence

proof end;

end;

registration

cluster strict Pappian Desarguesian Moufangian translational Fanoian AffinStruct ;
existence

proof end;

end;

registration

cluster strict Pappian Desarguesian Moufangian translational Fanoian AffinStruct ;
existence

proof end;

end;

registration

let OAS be OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like Fanoian ;
correctness by Th24;

end;

registration

let OAS be Pappian OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like Pappian Fanoian ;
correctness by Def11;

end;

registration

let OAS be Desarguesian OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like Desarguesian Fanoian ;
correctness by Def12;

end;

registration

let OAS be Moufangian OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like Moufangian Fanoian ;
correctness by Def13;

end;

registration

let OAS be translation OAffinSpace;
cluster Lambda OAS -> non trivial AffinSpace-like translational Fanoian ;
correctness by Def14;

end;