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