:: PAPDESAF semantic presentation

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

registration
let c1 be OAffinPlane;
cluster Lambda a1 -> non trivial AffinSpace-like 2-dimensional ;
correctness
coherence
Lambda c1 is 2-dimensional
;
by DIRAF:53;
end;

theorem Th1: :: PAPDESAF:1
canceled;

theorem Th2: :: PAPDESAF:2
for b1 being OAffinSpace
for b2 being set holds
( ( b2 is Element of b1 implies b2 is Element of (Lambda b1) ) & ( b2 is Element of (Lambda b1) implies b2 is Element of b1 ) & ( b2 is Subset of b1 implies b2 is Subset of (Lambda b1) ) & ( b2 is Subset of (Lambda b1) implies b2 is Subset of b1 ) )
proof end;

theorem Th3: :: PAPDESAF:3
for b1 being OAffinSpace
for b2, b3, b4 being Element of b1
for b5, b6, b7 being Element of (Lambda b1) st b2 = b5 & b3 = b6 & b4 = b7 holds
( LIN b2,b3,b4 iff LIN b5,b6,b7 )
proof end;

theorem Th4: :: PAPDESAF:4
for b1 being RealLinearSpace
for b2 being set holds
( b2 is Element of (OASpace b1) iff b2 is VECTOR of b1 )
proof end;

theorem Th5: :: PAPDESAF:5
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
for b3, b4, b5, b6 being Element of b2
for b7, b8, b9, b10 being VECTOR of b1 st b3 = b7 & b4 = b8 & b5 = b9 & b6 = b10 holds
( b3,b4 '||' b5,b6 iff b7,b8 '||' b9,b10 )
proof end;

theorem Th6: :: PAPDESAF:6
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
ex b3, b4 being VECTOR of b1 st
for b5, b6 being Real st (b5 * b3) + (b6 * b4) = 0. b1 holds
( b5 = 0 & b6 = 0 )
proof end;

notation
let c1 be AffinSpace;
synonym c1 satisfies_PAP' for Pappian c1c1 satisfies_PAPsatisfies_PAP ;
end;

notation
let c1 be AffinSpace;
synonym c1 satisfies_DES' for Desarguesian c1c1 satisfies_DESsatisfies_DES ;
end;

notation
let c1 be AffinSpace;
synonym c1 satisfies_TDES' for Moufangian c1c1 satisfies_TDESsatisfies_TDES ;
end;

notation
let c1 be AffinSpace;
synonym c1 satisfies_des' for translational c1c1 satisfies_dessatisfies_des ;
end;

notation
let c1 be AffinSpace;
synonym c1 satisfies_Fano for Fanoian c1c1 satisfies_Fanosatisfies_Fano ;
end;

definition
let c1 be AffinSpace;
canceled;
canceled;
canceled;
canceled;
redefine attr a1 is Fanoian means :Def5: :: PAPDESAF:def 5
for b1, b2, b3, b4 being Element of a1 st b1,b2 // b3,b4 & b1,b3 // b2,b4 & b1,b4 // b2,b3 holds
b1,b2 // b1,b3;
compatibility
( c1 satisfies_Fano iff for b1, b2, b3, b4 being Element of c1 st b1,b2 // b3,b4 & b1,b3 // b2,b4 & b1,b4 // b2,b3 holds
b1,b2 // b1,b3 )
proof end;
end;

:: deftheorem Def1 PAPDESAF:def 1 :
canceled;

:: deftheorem Def2 PAPDESAF:def 2 :
canceled;

:: deftheorem Def3 PAPDESAF:def 3 :
canceled;

:: deftheorem Def4 PAPDESAF:def 4 :
canceled;

:: deftheorem Def5 defines satisfies_Fano PAPDESAF:def 5 :
for b1 being AffinSpace holds
( b1 satisfies_Fano iff for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 & b2,b4 // b3,b5 & b2,b5 // b3,b4 holds
b2,b3 // b2,b4 );

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

:: deftheorem Def6 PAPDESAF:def 6 :
canceled;

:: deftheorem Def7 PAPDESAF:def 7 :
canceled;

:: deftheorem Def8 PAPDESAF:def 8 :
canceled;

:: deftheorem Def9 PAPDESAF:def 9 :
canceled;

:: deftheorem Def10 PAPDESAF:def 10 :
canceled;

:: deftheorem Def11 defines Pappian PAPDESAF:def 11 :
for b1 being OAffinSpace holds
( b1 is Pappian iff Lambda b1 satisfies_PAP' );

:: deftheorem Def12 defines Desarguesian PAPDESAF:def 12 :
for b1 being OAffinSpace holds
( b1 is Desarguesian iff Lambda b1 satisfies_DES' );

:: deftheorem Def13 defines Moufangian PAPDESAF:def 13 :
for b1 being OAffinSpace holds
( b1 is Moufangian iff Lambda b1 satisfies_TDES' );

:: deftheorem Def14 defines translation PAPDESAF:def 14 :
for b1 being OAffinSpace holds
( b1 is translation iff Lambda b1 satisfies_des' );

definition
let c1 be OAffinSpace;
attr a1 is satisfying_DES means :Def15: :: PAPDESAF:def 15
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1,b2 // b1,b5 & b1,b3 // b1,b6 & b1,b4 // b1,b7 & not LIN b1,b2,b3 & not LIN b1,b2,b4 & b2,b3 // b5,b6 & b2,b4 // b5,b7 holds
b3,b4 // b6,b7;
end;

:: deftheorem Def15 defines satisfying_DES PAPDESAF:def 15 :
for b1 being OAffinSpace holds
( b1 is satisfying_DES iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2,b3 // b2,b6 & b2,b4 // b2,b7 & b2,b5 // b2,b8 & not LIN b2,b3,b4 & not LIN b2,b3,b5 & b3,b4 // b6,b7 & b3,b5 // b6,b8 holds
b4,b5 // b7,b8 );

notation
let c1 be OAffinSpace;
synonym c1 satisfies_DES for satisfying_DES c1;
end;

definition
let c1 be OAffinSpace;
attr a1 is satisfying_DES_1 means :Def16: :: PAPDESAF:def 16
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b2,b1 // b1,b5 & b3,b1 // b1,b6 & b4,b1 // b1,b7 & not LIN b1,b2,b3 & not LIN b1,b2,b4 & b2,b3 // b6,b5 & b2,b4 // b7,b5 holds
b3,b4 // b7,b6;
end;

:: deftheorem Def16 defines satisfying_DES_1 PAPDESAF:def 16 :
for b1 being OAffinSpace holds
( b1 is satisfying_DES_1 iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b3,b2 // b2,b6 & b4,b2 // b2,b7 & b5,b2 // b2,b8 & not LIN b2,b3,b4 & not LIN b2,b3,b5 & b3,b4 // b7,b6 & b3,b5 // b8,b6 holds
b4,b5 // b8,b7 );

notation
let c1 be OAffinSpace;
synonym c1 satisfies_DES_1 for satisfying_DES_1 c1;
end;

theorem Th7: :: PAPDESAF:7
canceled;

theorem Th8: :: PAPDESAF:8
canceled;

theorem Th9: :: PAPDESAF:9
canceled;

theorem Th10: :: PAPDESAF:10
canceled;

theorem Th11: :: PAPDESAF:11
for b1 being OAffinSpace st b1 satisfies_DES_1 holds
b1 satisfies_DES
proof end;

theorem Th12: :: PAPDESAF:12
for b1 being OAffinSpace
for b2, b3, b4, b5, b6 being Element of the carrier of b1 st not LIN b2,b3,b4 & b3,b2 // b2,b5 & LIN b2,b4,b6 & b3,b4 '||' b5,b6 holds
( b4,b2 // b2,b6 & b3,b4 // b6,b5 )
proof end;

theorem Th13: :: PAPDESAF:13
for b1 being OAffinSpace
for b2, b3, b4, b5, b6 being Element of the carrier of b1 st not LIN b2,b3,b4 & b2,b3 // b2,b5 & LIN b2,b4,b6 & b3,b4 '||' b5,b6 holds
( b2,b4 // b2,b6 & b3,b4 // b5,b6 )
proof end;

theorem Th14: :: PAPDESAF:14
for b1 being OAffinSpace st b1 satisfies_DES_1 holds
Lambda b1 satisfies_DES'
proof end;

theorem Th15: :: PAPDESAF:15
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6 being VECTOR of b1
for b7 being Real st b2 - b3 = b7 * (b5 - b2) & b7 <> 0 & b2,b4 '||' b2,b6 & not b2,b3 '||' b2,b4 & b3,b4 '||' b5,b6 holds
( b6 = b5 + (((- b7) " ) * (b4 - b3)) & b6 = b2 + (((- b7) " ) * (b4 - b2)) & b4 - b3 = (- b7) * (b6 - b5) )
proof end;

Lemma17: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 st b2 <> b3 & b4 <> b3 & b2,b3 // b3,b4 holds
ex b5 being Real st
( b3 - b2 = b5 * (b4 - b3) & 0 < b5 )
proof end;

theorem Th16: :: PAPDESAF:16
canceled;

theorem Th17: :: PAPDESAF:17
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
b2 satisfies_DES_1
proof end;

theorem Th18: :: PAPDESAF:18
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
( b2 satisfies_DES_1 & b2 satisfies_DES )
proof end;

Lemma20: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 st b2,b3 '||' b2,b4 & b2 <> b3 & b2 <> b4 holds
ex b5 being Real st
( b3 - b2 = b5 * (b4 - b2) & b5 <> 0 )
proof end;

Lemma21: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds (b2 - b4) - (b3 - b4) = b2 - b3
proof end;

theorem Th19: :: PAPDESAF:19
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
Lambda b2 satisfies_PAP'
proof end;

theorem Th20: :: PAPDESAF:20
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
Lambda b2 satisfies_DES'
proof end;

theorem Th21: :: PAPDESAF:21
for b1 being AffinSpace st b1 satisfies_DES' holds
b1 satisfies_TDES'
proof end;

theorem Th22: :: PAPDESAF:22
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
Lambda b2 satisfies_TDES'
proof end;

theorem Th23: :: PAPDESAF:23
for b1 being RealLinearSpace
for b2 being OAffinSpace st b2 = OASpace b1 holds
Lambda b2 satisfies_des'
proof end;

theorem Th24: :: PAPDESAF:24
for b1 being OAffinSpace holds Lambda b1 satisfies_Fano
proof end;

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

registration
cluster strict Pappian Desarguesian Moufangian translational Fanoian AffinStruct ;
existence
ex b1 being AffinPlane st
( b1 is strict & b1 satisfies_Fano & b1 satisfies_PAP' & b1 satisfies_DES' & b1 satisfies_TDES' & b1 satisfies_des' )
proof end;
end;

registration
cluster strict Pappian Desarguesian Moufangian translational Fanoian AffinStruct ;
existence
ex b1 being AffinSpace st
( b1 is strict & b1 satisfies_Fano & b1 satisfies_PAP' & b1 satisfies_DES' & b1 satisfies_TDES' & b1 satisfies_des' )
proof end;
end;

registration
let c1 be OAffinSpace;
cluster Lambda a1 -> non trivial AffinSpace-like Fanoian ;
correctness
coherence
Lambda c1 satisfies_Fano
;
by Th24;
end;

registration
let c1 be Pappian OAffinSpace;
cluster Lambda a1 -> non trivial AffinSpace-like Pappian Fanoian ;
correctness
coherence
Lambda c1 satisfies_PAP'
;
by Def11;
end;

registration
let c1 be Desarguesian OAffinSpace;
cluster Lambda a1 -> non trivial AffinSpace-like Desarguesian Fanoian ;
correctness
coherence
Lambda c1 satisfies_DES'
;
by Def12;
end;

registration
let c1 be Moufangian OAffinSpace;
cluster Lambda a1 -> non trivial AffinSpace-like Moufangian Fanoian ;
correctness
coherence
Lambda c1 satisfies_TDES'
;
by Def13;
end;

registration
let c1 be translation OAffinSpace;
cluster Lambda a1 -> non trivial AffinSpace-like translational Fanoian ;
correctness
coherence
Lambda c1 satisfies_des'
;
by Def14;
end;