:: PAPDESAF semantic presentation
theorem Th1: :: PAPDESAF:1
canceled;
theorem Th2: :: PAPDESAF:2
theorem Th3: :: PAPDESAF:3
theorem Th4: :: PAPDESAF:4
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 )
theorem Th6: :: PAPDESAF:6
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 )
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 );
:: 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 :
:: deftheorem Def12 defines Desarguesian PAPDESAF:def 12 :
:: deftheorem Def13 defines Moufangian PAPDESAF:def 13 :
:: deftheorem Def14 defines translation PAPDESAF:def 14 :
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 );
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 );
theorem Th7: :: PAPDESAF:7
canceled;
theorem Th8: :: PAPDESAF:8
canceled;
theorem Th9: :: PAPDESAF:9
canceled;
theorem Th10: :: PAPDESAF:10
canceled;
theorem Th11: :: PAPDESAF:11
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 )
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 )
theorem Th14: :: PAPDESAF:14
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) )
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 )
theorem Th16: :: PAPDESAF:16
canceled;
theorem Th17: :: PAPDESAF:17
theorem Th18: :: PAPDESAF:18
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 )
Lemma21:
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds (b2 - b4) - (b3 - b4) = b2 - b3
theorem Th19: :: PAPDESAF:19
theorem Th20: :: PAPDESAF:20
theorem Th21: :: PAPDESAF:21
theorem Th22: :: PAPDESAF:22
theorem Th23: :: PAPDESAF:23
theorem Th24: :: PAPDESAF:24