AFF_2: Classical Configurations in Affine Planes

:: Classical Configurations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 13, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let AP be AffinPlane;

attr AP is satisfying_PPAP means :Def1: :: AFF_2:def 1
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;

end;

:: deftheorem Def1 defines satisfying_PPAP AFF_2:def 1 :

definition

let AP be AffinSpace;

attr AP is Pappian means :Def2: :: AFF_2:def 2
for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;

end;

:: deftheorem Def2 defines Pappian AFF_2:def 2 :

definition

let AP be AffinPlane;

attr AP is satisfying_PAP_1 means :Def3: :: AFF_2:def 3
for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N;

end;

:: deftheorem Def3 defines satisfying_PAP_1 AFF_2:def 3 :

definition

let AP be AffinSpace;

attr AP is Desarguesian means :Def4: :: AFF_2:def 4
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9;

end;

:: deftheorem Def4 defines Desarguesian AFF_2:def 4 :

definition

let AP be AffinPlane;

attr AP is satisfying_DES_1 means :Def5: :: AFF_2:def 5
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C;

end;

:: deftheorem Def5 defines satisfying_DES_1 AFF_2:def 5 :

definition

let AP be AffinPlane;

attr AP is satisfying_DES_2 means :: AFF_2:def 6
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 holds
c9 in C;

end;

:: deftheorem defines satisfying_DES_2 AFF_2:def 6 :

definition

let AP be AffinSpace;

attr AP is Moufangian means :Def7: :: AFF_2:def 7
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9;

end;

:: deftheorem Def7 defines Moufangian AFF_2:def 7 :

definition

let AP be AffinPlane;

attr AP is satisfying_TDES_1 means :Def8: :: AFF_2:def 8
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9;

end;

:: deftheorem Def8 defines satisfying_TDES_1 AFF_2:def 8 :

definition

let AP be AffinPlane;

attr AP is satisfying_TDES_2 means :Def9: :: AFF_2:def 9
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
a,b // a9,b9;

end;

:: deftheorem Def9 defines satisfying_TDES_2 AFF_2:def 9 :

definition

let AP be AffinPlane;

attr AP is satisfying_TDES_3 means :Def10: :: AFF_2:def 10
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K;

end;

:: deftheorem Def10 defines satisfying_TDES_3 AFF_2:def 10 :

definition

let AP be AffinSpace;

attr AP is translational means :Def11: :: AFF_2:def 11
for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9;

end;

:: deftheorem Def11 defines translational AFF_2:def 11 :

definition

let AP be AffinPlane;

attr AP is satisfying_des_1 means :Def12: :: AFF_2:def 12
for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C;

end;

:: deftheorem Def12 defines satisfying_des_1 AFF_2:def 12 :

definition

let AP be AffinSpace;

attr AP is satisfying_pap means :Def13: :: AFF_2:def 13
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;

end;

:: deftheorem Def13 defines satisfying_pap AFF_2:def 13 :

definition

let AP be AffinPlane;

attr AP is satisfying_pap_1 means :Def14: :: AFF_2:def 14
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N;

end;

:: deftheorem Def14 defines satisfying_pap_1 AFF_2:def 14 :

theorem :: AFF_2:1

for AP being AffinPlane holds
( AP is Pappian iff AP is satisfying_PAP_1 )

proof end;

theorem :: AFF_2:2

for AP being AffinPlane holds
( AP is Desarguesian iff AP is satisfying_DES_1 )

proof end;

theorem Th3: :: AFF_2:3

for AP being AffinPlane st AP is Moufangian holds
AP is satisfying_TDES_1

proof end;

theorem :: AFF_2:4

for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_TDES_2

proof end;

theorem :: AFF_2:5

for AP being AffinPlane st AP is satisfying_TDES_2 holds
AP is satisfying_TDES_3

proof end;

theorem :: AFF_2:6

for AP being AffinPlane st AP is satisfying_TDES_3 holds
AP is Moufangian

proof end;

theorem Th7: :: AFF_2:7

for AP being AffinPlane holds
( AP is translational iff AP is satisfying_des_1 )

proof end;

theorem :: AFF_2:8

for AP being AffinPlane holds
( AP is satisfying_pap iff AP is satisfying_pap_1 )

proof end;

theorem Th9: :: AFF_2:9

for AP being AffinPlane st AP is Pappian holds
AP is satisfying_pap

proof end;

theorem Th10: :: AFF_2:10

for AP being AffinPlane holds
( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )

proof end;

theorem :: AFF_2:11

for AP being AffinPlane st AP is Pappian holds
AP is Desarguesian

proof end;

theorem :: AFF_2:12

for AP being AffinPlane st AP is Desarguesian holds
AP is Moufangian

proof end;

theorem Th13: :: AFF_2:13

for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_des_1

proof end;

theorem :: AFF_2:14

for AP being AffinPlane st AP is Moufangian holds
AP is translational

proof end;

theorem :: AFF_2:15

for AP being AffinPlane st AP is translational holds
AP is satisfying_pap

proof end;