:: Classical Configurations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 13, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DIRAF, SUBSET_1, AFF_1, ANALOAF, INCSP_1, AFF_2;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1;
constructors AFF_1;
registrations STRUCT_0;
begin
reserve AP for AffinPlane,
a,a9,b,b9,c,c9,x,y,o,p,q,r,s for Element of AP,
A,C,C9,D,K,M,N,P,T for Subset of AP;
definition
let AP;
attr AP is satisfying_PPAP means
:: AFF_2:def 1
for M,N,a,b,c,a9,b9,c9 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;
definition
let AP be AffinSpace;
attr AP is Pappian means
:: AFF_2:def 2
for M,N being Subset of AP, 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;
definition
let AP;
attr AP is satisfying_PAP_1 means
:: AFF_2:def 3
for M,N,o,a,b,c,a9,b9,c9 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;
definition
let AP be AffinSpace;
attr AP is Desarguesian means
:: AFF_2:def 4
for A,P,C being Subset of AP, 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;
definition
let AP;
attr AP is satisfying_DES_1 means
:: AFF_2:def 5
for A,P,C,o,a,b,c,a9,b9,c9 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;
definition
let AP;
attr AP is satisfying_DES_2 means
:: AFF_2:def 6
for A,P,C,o,a,b,c,a9,b9,c9 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;
definition
let AP be AffinSpace;
attr AP is Moufangian means
:: AFF_2:def 7
for K being Subset of AP, 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;
definition
let AP;
attr AP is satisfying_TDES_1 means
:: AFF_2:def 8
for K,o,a,b,c,a9,b9,c9 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;
definition
let AP;
attr AP is satisfying_TDES_2 means
:: AFF_2:def 9
for K,o,a,b,c,a9,b9,c9 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;
definition
let AP;
attr AP is satisfying_TDES_3 means
:: AFF_2:def 10
for K,o,a,b,c,a9,b9,c9 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;
definition
let AP be AffinSpace;
attr AP is translational means
:: AFF_2:def 11
for A,P,C being Subset of AP, 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;
definition
let AP;
attr AP is satisfying_des_1 means
:: AFF_2:def 12
for A,P,C,a,b,c,a9,b9,c9 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;
definition
let AP be AffinSpace;
attr AP is satisfying_pap means
:: AFF_2:def 13
for M,N being Subset of AP, 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;
definition
let AP;
attr AP is satisfying_pap_1 means
:: AFF_2:def 14
for M,N,a,b,c,a9,b9,c9 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;
theorem :: AFF_2:1
AP is Pappian iff AP is satisfying_PAP_1;
theorem :: AFF_2:2
AP is Desarguesian iff AP is satisfying_DES_1;
theorem :: AFF_2:3
AP is Moufangian implies AP is satisfying_TDES_1;
theorem :: AFF_2:4
AP is satisfying_TDES_1 implies AP is satisfying_TDES_2;
theorem :: AFF_2:5
AP is satisfying_TDES_2 implies AP is satisfying_TDES_3;
theorem :: AFF_2:6
AP is satisfying_TDES_3 implies AP is Moufangian;
theorem :: AFF_2:7
AP is translational iff AP is satisfying_des_1;
theorem :: AFF_2:8
AP is satisfying_pap iff AP is satisfying_pap_1;
theorem :: AFF_2:9
AP is Pappian implies AP is satisfying_pap;
theorem :: AFF_2:10
AP is satisfying_PPAP iff AP is Pappian & AP is satisfying_pap;
theorem :: AFF_2:11
AP is Pappian implies AP is Desarguesian;
theorem :: AFF_2:12
AP is Desarguesian implies AP is Moufangian;
theorem :: AFF_2:13
AP is satisfying_TDES_1 implies AP is satisfying_des_1;
theorem :: AFF_2:14
AP is Moufangian implies AP is translational;
theorem :: AFF_2:15
AP is translational implies AP is satisfying_pap;