:: Affine Localizations of Desargues Axiom
:: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 26, 1990
:: Copyright (c) 1990-2017 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, AFF_3;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2;
constructors AFF_1, AFF_2;
registrations STRUCT_0;
begin
reserve AP for AffinPlane;
reserve a,a9,b,b9,c,c9,d,x,y,o,p,q for Element of AP;
reserve A,C,D9,M,N,P for Subset of AP;
definition
let AP;
attr AP is satisfying_DES1 means
:: AFF_3:def 1
for A,P,C,o,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in A
& a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o
<>a & o<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & a<>a9 & LIN b,a,p
& LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q;
end;
definition
let AP;
attr AP is satisfying_DES1_1 means
:: AFF_3:def 2
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C &
o<>a & o<>b & o<>c & p<>q & c <>q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,
p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9;
end;
definition
let AP;
attr AP is satisfying_DES1_2 means
:: AFF_3:def 3
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o<>a & o
<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & c <>c9 & LIN b,a,p & LIN
b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C;
end;
definition
let AP;
attr AP is satisfying_DES1_3 means
:: AFF_3:def 4
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o<>a & o
<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & b<>b9 & a<>a9 & LIN b,a,
p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o
in P;
end;
definition
let AP;
attr AP is satisfying_DES2 means
:: AFF_3:def 5
for A,P,C,a,a9,b,b9,c,c9,p,q st A is
being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A &
a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c
& not LIN b9,a9,c9 & p<>q & a<>a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN
b9,c9,q & a,c // a9,c9 holds a,c // p,q;
end;
definition
let AP;
attr AP is satisfying_DES2_1 means
:: AFF_3:def 6
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a
,c & not LIN b9,a9,c9 & p<>q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,
q & a,c // p,q holds a,c // a9,c9;
end;
definition
let AP;
attr AP is satisfying_DES2_2 means
:: AFF_3:def 7
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not
LIN b9,a9,c9 & p<>q & a<>a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q
& a,c // a9,c9 & a,c // p,q holds A // P;
end;
definition
let AP;
attr AP is satisfying_DES2_3 means
:: AFF_3:def 8
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not
LIN b9,a9,c9 & p<>q & c <>c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,
q & a,c // a9,c9 & a,c // p,q holds A // C;
end;
theorem :: AFF_3:1
AP is satisfying_DES1 implies AP is satisfying_DES1_1;
theorem :: AFF_3:2
AP is satisfying_DES1_1 implies AP is satisfying_DES1;
theorem :: AFF_3:3
AP is Desarguesian implies AP is satisfying_DES1;
theorem :: AFF_3:4
AP is Desarguesian implies AP is satisfying_DES1_2;
theorem :: AFF_3:5
AP is satisfying_DES1_2 implies AP is satisfying_DES1_3;
theorem :: AFF_3:6
AP is satisfying_DES1_2 implies AP is Desarguesian;
theorem :: AFF_3:7
AP is satisfying_DES2_1 implies AP is satisfying_DES2;
theorem :: AFF_3:8
AP is satisfying_DES2_1 iff AP is satisfying_DES2_3;
theorem :: AFF_3:9
AP is satisfying_DES2 iff AP is satisfying_DES2_2;
theorem :: AFF_3:10
AP is satisfying_DES1_3 implies AP is satisfying_DES2_1;