:: Classical Configurations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 13, 1990
:: Copyright (c) 1990-2026 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;
theorems AFF_1;
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
AP is Pappian iff AP is satisfying_PAP_1
proof
hereby assume
A1: AP is Pappian;
thus AP is satisfying_PAP_1
proof
let M,N,o,a,b,c,a9,b9,c9;
assume that
A2: M is being_line and
A3: N is being_line and
A4: M<>N and
A5: o in M and
A6: o in N and
A7: o<>a and
o<>a9 and
A8: o<>b and
A9: o<>b9 and
A10: o<>c and
A11: o<>c9 and
A12: a in M and
A13: b in M and
A14: c in M and
A15: b9 in N and
A16: c9 in N and
A17: a,b9 // b,a9 and
A18: b,c9 // c,b9 and
A19: a,c9 // c,a9 and
A20: b<>c;
A21: a<>c9 by A2,A3,A4,A5,A6,A7,A12,A16,AFF_1:18;
A22: b<>a9
proof
assume b=a9;
then c,b // a,c9 by A19,AFF_1:4;
then c9 in M by A2,A12,A13,A14,A20,AFF_1:48;
hence contradiction by A2,A3,A4,A5,A6,A11,A16,AFF_1:18;
end;
not b,a9 // N
proof
assume
A23: b,a9 // N;
b,a9 // a,b9 by A17,AFF_1:4;
then a,b9 // N by A22,A23,AFF_1:32;
then b9,a // N by AFF_1:34;
then a in N by A3,A15,AFF_1:23;
hence contradiction by A2,A3,A4,A5,A6,A7,A12,AFF_1:18;
end;
then consider x such that
A24: x in N and
A25: LIN b,a9,x by A3,AFF_1:59;
A26: b,a9 // b,x by A25,AFF_1:def 1;
A27: o<>x
proof
assume o=x;
then b,o // a,b9 by A17,A22,A26,AFF_1:5;
then b9 in M by A2,A5,A8,A12,A13,AFF_1:48;
hence contradiction by A2,A3,A4,A5,A6,A9,A15,AFF_1:18;
end;
a,b9 // b,x by A17,A22,A26,AFF_1:5;
then a,c9 // c,x by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15
,A16,A18,A24,A27;
then c,a9 // c,x by A19,A21,AFF_1:5;
then LIN c,a9,x by AFF_1:def 1;
then
A28: LIN a9,x,c by AFF_1:6;
A29: LIN a9,x,x by AFF_1:7;
assume
A30: not a9 in N;
LIN a9,x,b by A25,AFF_1:6;
then x in M by A2,A13,A14,A20,A30,A24,A28,A29,AFF_1:8,25;
hence contradiction by A2,A3,A4,A5,A6,A24,A27,AFF_1:18;
end;
end;
assume
A31: AP is satisfying_PAP_1;
let M,N,o,a,b,c,a9,b9,c9;
assume that
A32: M is being_line and
A33: N is being_line and
A34: M<>N & o in M & o in N and
A35: o<>a and
A36: o<>a9 and
A37: o<>b and
A38: o<>b9 and
A39: o<>c & o<>c9 and
A40: a in M and
A41: b in M and
A42: c in M and
A43: a9 in N and
A44: b9 in N and
A45: c9 in N and
A46: a,b9 // b,a9 and
A47: b,c9 // c,b9;
set A=Line(a,c9), P=Line(b,a9);
A48: b<>a9 by A32,A33,A34,A36,A41,A43,AFF_1:18;
then
A49: b in P by AFF_1:24;
assume
A50: not a,c9 // c,a9;
then
A51: a<>c9 by AFF_1:3;
then
A52: a in A & c9 in A by AFF_1:24;
A53: a9 in P by A48,AFF_1:24;
A is being_line by A51,AFF_1:24;
then consider K such that
A54: c in K and
A55: A // K by AFF_1:49;
A56: b<>c
proof
assume
A57: b=c;
then LIN b,c9,b9 by A47,AFF_1:def 1;
then LIN b9,c9,b by AFF_1:6;
then b9=c9 or b in N by A33,A44,A45,AFF_1:25;
hence contradiction by A32,A33,A34,A37,A41,A46,A50,A57,AFF_1:18;
end;
A58: b9<>c9
proof
assume b9=c9;
then b9,b // b9,c by A47,AFF_1:4;
then LIN b9,b,c by AFF_1:def 1;
then LIN b,c,b9 by AFF_1:6;
then b9 in M by A32,A41,A42,A56,AFF_1:25;
hence contradiction by A32,A33,A34,A38,A44,AFF_1:18;
end;
A59: not P // K
proof
assume P // K;
then P // A by A55,AFF_1:44;
then b,a9 // a,c9 by A52,A49,A53,AFF_1:39;
then a,b9 // a,c9 by A46,A48,AFF_1:5;
then LIN a,b9,c9 by AFF_1:def 1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A33,A44,A45,A58,AFF_1:25;
hence contradiction by A32,A33,A34,A35,A40,AFF_1:18;
end;
A60: P is being_line by A48,AFF_1:24;
K is being_line by A55,AFF_1:36;
then consider x such that
A61: x in P and
A62: x in K by A60,A59,AFF_1:58;
A63: a,c9 // c,x by A52,A54,A55,A62,AFF_1:39;
LIN b,x,a9 by A60,A49,A53,A61,AFF_1:21;
then b,x // b,a9 by AFF_1:def 1;
then a,b9 // b,x by A46,A48,AFF_1:5;
then x in N by A31,A32,A33,A34,A35,A37,A38,A39,A40,A41,A42,A44,A45,A47
,A56,A63;
then N=P by A33,A43,A50,A60,A53,A61,A63,AFF_1:18;
hence contradiction by A32,A33,A34,A37,A41,A49,AFF_1:18;
end;
theorem
AP is Desarguesian iff AP is satisfying_DES_1
proof
hereby assume
A1: AP is Desarguesian;
thus AP is satisfying_DES_1
proof
let A,P,C,o,a,b,c,a9,b9,c9;
assume that
A2: o in A and
A3: o in P and
A4: o<>a and
A5: o<>b and
o<>c and
A6: a in A and
A7: a9 in A and
A8: b in P and
A9: b9 in P and
A10: c in C and
A11: c9 in C and
A12: A is being_line and
A13: P is being_line and
A14: C is being_line and
A15: A<>P and
A16: A<>C and
A17: a,b // a9,b9 and
A18: a,c // a9,c9 and
A19: b,c // b9,c9 and
A20: not LIN a,b,c and
A21: c <>c9;
set K=Line(o,c9);
assume
A22: not o in C;
then
A23: K is being_line by A11,AFF_1:24;
A24: a9<>c9
proof
assume
A25: a9=c9;
then b,c // a9,b9 by A19,AFF_1:4;
then a,b // b,c or a9=b9 by A17,AFF_1:5;
then b,a // b,c or a9=b9 by AFF_1:4;
then LIN b,a,c or a9=b9 by AFF_1:def 1;
hence contradiction by A2,A3,A7,A9,A11,A12,A13,A15,A20,A22,A25,AFF_1:6
,18;
end;
A26: A<>K
proof
assume A=K;
then
A27: c9 in A by A2,AFF_1:24;
a9,c9 // a,c by A18,AFF_1:4;
then c in A by A6,A7,A12,A24,A27,AFF_1:48;
hence contradiction by A10,A11,A12,A14,A16,A21,A27,AFF_1:18;
end;
A28: a<>c by A20,AFF_1:7;
A29: o in K by A11,A22,AFF_1:24;
A30: c9 in K by A11,A22,AFF_1:24;
not a,c // K
proof
assume a,c // K;
then a9,c9 // K by A18,A28,AFF_1:32;
then c9,a9 // K by AFF_1:34;
then a9 in K by A23,A30,AFF_1:23;
then
A31: a9 in P by A2,A3,A7,A12,A23,A29,A26,AFF_1:18;
a9,b9 // b,a by A17,AFF_1:4;
then a9=b9 or a in P by A8,A9,A13,A31,AFF_1:48;
then a,c // b,c by A2,A3,A4,A6,A12,A13,A15,A18,A19,A24,AFF_1:5,18;
then c,a // c,b by AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A20,AFF_1:6;
end;
then consider x such that
A32: x in K and
A33: LIN a,c,x by A23,AFF_1:59;
A34: o<>x
proof
assume o=x;
then LIN a,o,c by A33,AFF_1:6;
then
A35: c in A by A2,A4,A6,A12,AFF_1:25;
then c9 in A by A6,A7,A12,A18,A28,AFF_1:48;
hence contradiction by A10,A11,A12,A14,A16,A21,A35,AFF_1:18;
end;
A36: b9<>c9
proof
assume b9=c9;
then a9=b9 or a,c // a,b by A17,A18,AFF_1:5;
then a9=b9 or LIN a,c,b by AFF_1:def 1;
then b,c // a,c by A18,A19,A20,A24,AFF_1:5,6;
then c,b // c,a by AFF_1:4;
then LIN c,b,a by AFF_1:def 1;
hence contradiction by A20,AFF_1:6;
end;
A37: a,c // a,x by A33,AFF_1:def 1;
then a,x // a9,c9 by A18,A28,AFF_1:5;
then
b,x // b9,c9 by A1,A2,A3,A4,A5,A6,A7,A8,A9,A12,A13,A15,A17,A23,A29,A30,A26,A32
,A34;
then
A38: b,x // b,c by A19,A36,AFF_1:5;
A39: not LIN a,b,x
proof
assume LIN a,b,x;
then a,b // a,x by AFF_1:def 1;
then a,b // a,c or a=x by A37,AFF_1:5;
hence contradiction by A2,A4,A6,A12,A20,A23,A29,A26,A32,AFF_1:18,def 1;
end;
LIN a,x,c by A33,AFF_1:6;
then c in K by A32,A39,A38,AFF_1:14;
hence contradiction by A10,A11,A14,A21,A22,A23,A29,A30,AFF_1:18;
end;
end;
assume
A40: AP is satisfying_DES_1;
let A,P,C,o,a,b,c,a9,b9,c9;
assume that
A41: o in A and
A42: o in P and
A43: o in C and
A44: o<>a and
A45: o<>b and
A46: o<>c and
A47: a in A and
A48: a9 in A and
A49: b in P and
A50: b9 in P and
A51: c in C and
A52: c9 in C and
A53: A is being_line and
A54: P is being_line and
A55: C is being_line and
A56: A<>P and
A57: A<>C and
A58: a,b // a9,b9 and
A59: a,c // a9,c9;
assume
A60: not b,c // b9,c9;
A61: a9<>b9
proof
A62: a9,c9 // c,a by A59,AFF_1:4;
assume
A63: a9=b9;
then a9 in C by A41,A42,A43,A48,A50,A53,A54,A56,AFF_1:18;
then a in C or a9=c9 by A51,A52,A55,A62,AFF_1:48;
hence contradiction by A41,A43,A44,A47,A53,A55,A57,A60,A63,AFF_1:3,18;
end;
A64: a9<>c9
proof
assume a9=c9;
then
A65: a9 in P by A41,A42,A43,A48,A52,A53,A55,A57,AFF_1:18;
a9,b9 // b,a by A58,AFF_1:4;
then a in P by A49,A50,A54,A61,A65,AFF_1:48;
hence contradiction by A41,A42,A44,A47,A53,A54,A56,AFF_1:18;
end;
A66: o<>c9
proof
assume
A67: o=c9;
a9,c9 // a,c by A59,AFF_1:4;
then c in A by A41,A47,A48,A53,A64,A67,AFF_1:48;
hence contradiction by A41,A43,A46,A51,A53,A55,A57,AFF_1:18;
end;
set M=Line(a,c), N=Line(b9,c9);
A68: a<>c by A41,A43,A44,A47,A51,A53,A55,A57,AFF_1:18;
then
A69: c in M by AFF_1:24;
A70: a<>b by A41,A42,A44,A47,A49,A53,A54,A56,AFF_1:18;
A71: not LIN a9,b9,c9
proof
assume
A72: LIN a9,b9,c9;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A59,A64,AFF_1:5;
then a,b // a,c by A58,A61,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A73: b,c // a9,b9 by A58,A70,AFF_1:5;
LIN b9,c9,a9 by A72,AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A60,A61,A73,AFF_1:5;
end;
A74: b9<>c9 by A60,AFF_1:3;
then
A75: b9 in N & c9 in N by AFF_1:24;
N is being_line by A74,AFF_1:24;
then consider D such that
A76: b in D and
A77: N // D by AFF_1:49;
A78: a in M by A68,AFF_1:24;
A79: not M // D
proof
assume M // D;
then M // N by A77,AFF_1:44;
then a,c // b9,c9 by A78,A69,A75,AFF_1:39;
then a9,c9 // b9,c9 by A59,A68,AFF_1:5;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def 1;
hence contradiction by A71,AFF_1:6;
end;
A80: M is being_line by A68,AFF_1:24;
D is being_line by A77,AFF_1:36;
then consider x such that
A81: x in M and
A82: x in D by A80,A79,AFF_1:58;
LIN a,c,x by A80,A78,A69,A81,AFF_1:21;
then a,c // a,x by AFF_1:def 1;
then
A83: a,x // a9,c9 by A59,A68,AFF_1:5;
set T=Line(c9,x);
A84: a<>a9
proof
assume
A85: a=a9;
then LIN a,c,c9 by A59,AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then
A86: c =c9 or a in C by A51,A52,A55,AFF_1:25;
LIN a,b,b9 by A58,A85,AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b=b9 or a in P by A49,A50,A54,AFF_1:25;
hence contradiction by A41,A42,A43,A44,A47,A53,A54,A55,A56,A57,A60,A86,
AFF_1:2,18;
end;
A87: x<>c9
proof
assume x=c9;
then c9,a // c9,a9 by A83,AFF_1:4;
then LIN c9,a,a9 by AFF_1:def 1;
then LIN a,a9,c9 by AFF_1:6;
then c9 in A by A47,A48,A53,A84,AFF_1:25;
hence contradiction by A41,A43,A52,A53,A55,A57,A66,AFF_1:18;
end;
then
A88: T is being_line & c9 in T by AFF_1:24;
A89: b,x // b9,c9 by A75,A76,A77,A82,AFF_1:39;
A90: x in T by A87,AFF_1:24;
A91: a<>x
proof
assume a=x;
then a,b // b9,c9 by A75,A76,A77,A82,AFF_1:39;
then a9,b9 // b9,c9 by A58,A70,AFF_1:5;
then b9,a9 // b9,c9 by AFF_1:4;
then LIN b9,a9,c9 by AFF_1:def 1;
hence contradiction by A71,AFF_1:6;
end;
not LIN a,b,x
proof
assume LIN a,b,x;
then a,b // a,x by AFF_1:def 1;
then a,b // a9,c9 by A83,A91,AFF_1:5;
then a9,b9 // a9,c9 by A58,A70,AFF_1:5;
hence contradiction by A71,AFF_1:def 1;
end;
then o in T by A40,A41,A42,A44,A45,A47,A48,A49,A50,A53,A54,A56,A58,A83
,A89,A87,A88,A90;
then x in C by A43,A52,A55,A66,A88,A90,AFF_1:18;
then C=M by A51,A55,A60,A80,A69,A81,A89,AFF_1:18;
hence contradiction by A41,A43,A44,A47,A53,A55,A57,A78,AFF_1:18;
end;
theorem Th3:
AP is Moufangian implies AP is satisfying_TDES_1
proof
assume
A1: AP is Moufangian;
let K,o,a,b,c,a9,b9,c9;
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o<>c and
A8: a<>b and
A9: LIN o,a,a9 and
A10: a,b // a9,b9 and
A11: b,c // b9,c9 and
A12: a,c // a9,c9 and
A13: a,b // K;
consider P such that
A14: a9 in P and
A15: K // P by A2,AFF_1:49;
A16: P is being_line by A15,AFF_1:36;
set A=Line(o,b), C=Line(o,a);
A17: o in A & b in A by AFF_1:15;
assume
A18: not LIN o,b,b9;
then o<>b by AFF_1:7;
then
A19: A is being_line by AFF_1:def 3;
A20: not b in K by A6,A13,AFF_1:35;
not A // P
proof
assume A // P;
then A // K by A15,AFF_1:44;
hence contradiction by A3,A20,A17,AFF_1:45;
end;
then consider x such that
A21: x in A and
A22: x in P by A19,A16,AFF_1:58;
A23: o in C & a in C by AFF_1:15;
A24: LIN o,b,x by A19,A17,A21,AFF_1:21;
a,b // P by A13,A15,AFF_1:43;
then a9,b9 // P by A8,A10,AFF_1:32;
then
A25: b9 in P by A14,A16,AFF_1:23;
then
A26: LIN b9,x,b9 by A16,A22,AFF_1:21;
A27: C is being_line by A3,A6,AFF_1:def 3;
then
A28: a9 in C by A3,A6,A9,A23,AFF_1:25;
A29: b9<>c9
proof
A30: a9,c9 // c,a by A12,AFF_1:4;
assume
A31: b9=c9;
then P=K by A5,A15,A25,AFF_1:45;
then a9=o by A2,A3,A6,A27,A23,A28,A14,AFF_1:18;
then b9=o by A2,A3,A4,A5,A6,A31,A30,AFF_1:48;
hence contradiction by A18,AFF_1:7;
end;
A32: b<>c by A4,A6,A13,AFF_1:35;
a9,x // K by A14,A15,A22,AFF_1:40;
then a,b // a9,x by A2,A13,AFF_1:31;
then b,c // x,c9 by A1,A2,A3,A4,A5,A6,A7,A8,A9,A12,A13,A24;
then b9,c9 // x,c9 by A11,A32,AFF_1:5;
then c9,b9 // c9,x by AFF_1:4;
then LIN c9,b9,x by AFF_1:def 1;
then
A33: LIN b9,x,c9 by AFF_1:6;
A34: a9<>b9
proof
assume
A35: a9=b9;
A36: now
assume a9=c9;
then b9=o by A2,A3,A5,A6,A27,A23,A28,A35,AFF_1:18;
hence contradiction by A18,AFF_1:7;
end;
a,c // b,c or a9=c9 by A11,A12,A35,AFF_1:5;
then c,a // c,b by A36,AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
then LIN a,c,b by AFF_1:6;
then a,c // a,b by AFF_1:def 1;
then a,b // a,c by AFF_1:4;
then a,c // K by A8,A13,AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2,A4,A6,AFF_1:23;
end;
LIN b9,x,a9 by A14,A16,A22,A25,AFF_1:21;
then LIN b9,c9,a9 by A18,A24,A33,A26,AFF_1:8;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
then b,c // a9,b9 by A11,A29,AFF_1:5;
then a,b // b,c by A10,A34,AFF_1:5;
then b,c // K by A8,A13,AFF_1:32;
then c,b // K by AFF_1:34;
hence contradiction by A2,A4,A20,AFF_1:23;
end;
theorem
AP is satisfying_TDES_1 implies AP is satisfying_TDES_2
proof
assume
A1: AP is satisfying_TDES_1;
let K,o,a,b,c,a9,b9,c9;
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o<>c and
A8: a<>b and
A9: LIN o,a,a9 and
A10: LIN o,b,b9 and
A11: b,c // b9,c9 and
A12: a,c // a9,c9 and
A13: a,b // K;
set A=Line(o,a), P=Line(o,b);
A14: A is being_line & a in A by A3,A6,AFF_1:24;
A15: o in A by A3,A6,AFF_1:24;
then
A16: a9 in A by A3,A6,A9,A14,AFF_1:25;
A17: o<>b by A3,A6,A13,AFF_1:35;
then
A18: P is being_line by AFF_1:24;
consider N such that
A19: a9 in N and
A20: K // N by A2,AFF_1:49;
A21: N is being_line by A20,AFF_1:36;
set T=Line(b9,c9);
A22: not b in K by A6,A13,AFF_1:35;
A23: b in P by A17,AFF_1:24;
A24: o in P by A17,AFF_1:24;
then
A25: b9 in P by A10,A17,A18,A23,AFF_1:25;
assume
A26: not a,b // a9,b9;
then
A27: a9<>b9 by AFF_1:3;
A28: not b9 in K
proof
A29: a9,c9 // a,c by A12,AFF_1:4;
A30: b9,c9 // c,b by A11,AFF_1:4;
assume
A31: b9 in K;
then b9=o by A2,A3,A22,A18,A24,A23,A25,AFF_1:18;
then c9 in A by A2,A3,A4,A5,A22,A15,A30,AFF_1:48;
then a9=c9 or c in A by A14,A16,A29,AFF_1:48;
hence contradiction by A2,A3,A4,A5,A6,A7,A27,A22,A15,A14,A31,A30,AFF_1:18
,48;
end;
then
A32: T is being_line by A5,AFF_1:24;
A33: b9 in T by A5,A28,AFF_1:24;
A34: c9 in T by A5,A28,AFF_1:24;
not N // T
proof
assume N // T;
then K // T by A20,AFF_1:44;
hence contradiction by A5,A28,A33,A34,AFF_1:45;
end;
then consider x such that
A35: x in N and
A36: x in T by A32,A21,AFF_1:58;
a9,x // K by A19,A20,A35,AFF_1:40;
then
A37: a,b // a9,x by A2,A13,AFF_1:31;
LIN c9,b9,x by A32,A33,A34,A36,AFF_1:21;
then c9,b9 // c9,x by AFF_1:def 1;
then b9,c9 // x,c9 by AFF_1:4;
then b,c // x,c9 by A5,A11,A28,AFF_1:5;
then LIN o,b,x by A1,A2,A3,A4,A5,A6,A7,A8,A9,A12,A13,A37;
then x in P by A17,A18,A24,A23,AFF_1:25;
then P=T by A26,A18,A25,A32,A33,A36,A37,AFF_1:18;
then LIN c9,b9,b by A18,A23,A33,A34,AFF_1:21;
then c9,b9 // c9,b by AFF_1:def 1;
then b9,c9 // b,c9 by AFF_1:4;
then b,c // b,c9 by A5,A11,A28,AFF_1:5;
then LIN b,c,c9 by AFF_1:def 1;
then
A38: LIN c,c9,b by AFF_1:6;
then a,c // a9,c by A2,A4,A5,A12,A22,AFF_1:25;
then c,a // c,a9 by AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then
A39: a=a9 or c in A by A14,A16,AFF_1:25;
b,c // b9,c by A2,A4,A5,A11,A22,A38,AFF_1:25;
then c,b // c,b9 by AFF_1:4;
then LIN c,b,b9 by AFF_1:def 1;
then LIN b,b9,c by AFF_1:6;
then b=b9 or c in P by A18,A23,A25,AFF_1:25;
hence contradiction by A2,A3,A4,A6,A7,A26,A22,A18,A15,A14,A24,A23,A39,
AFF_1:2,18;
end;
theorem
AP is satisfying_TDES_2 implies AP is satisfying_TDES_3
proof
assume
A1: AP is satisfying_TDES_2;
let K,o,a,b,c,a9,b9,c9;
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: not a in K and
A6: o<>c and
A7: a<>b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: a,b // a9,b9 and
A11: a,c // a9,c9 and
A12: b,c // b9,c9 and
A13: a,b // K;
set A=Line(o,a), P=Line(o,b), N=Line(b,c);
A14: o in A by A3,A5,AFF_1:24;
A15: not LIN a,b,c
proof
assume LIN a,b,c;
then a,b // a,c by AFF_1:def 1;
then a,c // K by A7,A13,AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2,A4,A5,AFF_1:23;
end;
A16: o<>b by A3,A5,A13,AFF_1:35;
then
A17: b in P by AFF_1:24;
A18: a9,b9 // b,a by A10,AFF_1:4;
A19: b<>c by A4,A5,A13,AFF_1:35;
then
A20: b in N & c in N by AFF_1:24;
A21: a in A by A3,A5,AFF_1:24;
A22: A is being_line by A3,A5,AFF_1:24;
A23: A<>P
proof
assume A=P;
then a,b // A by A22,A21,A17,AFF_1:40,41;
hence contradiction by A3,A5,A7,A13,A14,A21,AFF_1:45,53;
end;
assume
A24: not c9 in K;
A25: P is being_line by A16,AFF_1:24;
A26: o in P by A16,AFF_1:24;
then
A27: b9 in P by A9,A16,A25,A17,AFF_1:25;
A28: a9 in A by A3,A5,A8,A22,A14,A21,AFF_1:25;
A29: a9<>b9
proof
assume
A30: a9=b9;
then a,c // b,c or a9=c9 by A11,A12,AFF_1:5;
then c,a // c,b or a9=c9 by AFF_1:4;
then LIN c,a,b or a9=c9 by AFF_1:def 1;
hence contradiction by A3,A24,A15,A22,A25,A14,A26,A28,A27,A23,A30,AFF_1:6
,18;
end;
A31: a9<>c9
proof
assume a9=c9;
then b,c // a9,b9 by A12,AFF_1:4;
then a,b // b,c by A10,A29,AFF_1:5;
then b,a // b,c by AFF_1:4;
then LIN b,a,c by AFF_1:def 1;
hence contradiction by A15,AFF_1:6;
end;
not a9,c9 // K
proof
assume
A32: a9,c9 // K;
a9,c9 // a,c by A11,AFF_1:4;
then a,c // K by A31,A32,AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2,A4,A5,AFF_1:23;
end;
then consider x such that
A33: x in K and
A34: LIN a9,c9,x by A2,AFF_1:59;
a9,c9 // a9,x by A34,AFF_1:def 1;
then
A35: a,c // a9,x by A11,A31,AFF_1:5;
N is being_line by A19,AFF_1:24;
then consider T such that
A36: x in T and
A37: N // T by AFF_1:49;
A38: not b in K by A5,A13,AFF_1:35;
A39: not T // P
proof
assume T // P;
then N // P by A37,AFF_1:44;
then c in P by A17,A20,AFF_1:45;
hence contradiction by A2,A3,A4,A6,A38,A25,A26,A17,AFF_1:18;
end;
T is being_line by A37,AFF_1:36;
then consider y such that
A40: y in T and
A41: y in P by A25,A39,AFF_1:58;
A42: b,c // y,x by A20,A36,A37,A40,AFF_1:39;
A43: now
assume y=b9;
then b9,c9 // b9,x by A12,A19,A42,AFF_1:5;
then LIN b9,c9,x by AFF_1:def 1;
then
A44: LIN c9,x,b9 by AFF_1:6;
LIN c9,x,a9 & LIN c9,x,c9 by A34,AFF_1:6,7;
then LIN a9,b9,c9 by A24,A33,A44,AFF_1:8;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A11,A31,AFF_1:5;
then a,b // a,c by A10,A29,AFF_1:5;
hence contradiction by A15,AFF_1:def 1;
end;
LIN o,b,y by A25,A26,A17,A41,AFF_1:21;
then a,b // a9,y by A1,A2,A3,A4,A5,A6,A7,A8,A13,A33,A42,A35;
then a9,b9 // a9,y by A7,A10,AFF_1:5;
then LIN a9,b9,y by AFF_1:def 1;
then LIN b9,y,a9 by AFF_1:6;
then a9 in P by A25,A27,A41,A43,AFF_1:25;
then a in P by A25,A17,A27,A29,A18,AFF_1:48;
hence contradiction by A3,A5,A25,A26,A23,AFF_1:24;
end;
theorem
AP is satisfying_TDES_3 implies AP is Moufangian
proof
assume
A1: AP is satisfying_TDES_3;
let K,o,a,b,c,a9,b9,c9;
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o<>c and
A8: a<>b and
A9: LIN o,a,a9 and
A10: LIN o,b,b9 and
A11: a,b // a9,b9 and
A12: a,c // a9,c9 and
A13: a,b // K;
set A=Line(o,a), P=Line(o,b), M=Line(b,c), T=Line(a9,c9);
A14: o in A by A3,A6,AFF_1:24;
assume
A15: not b,c // b9,c9;
then
A16: b<>c by AFF_1:3;
then
A17: b in M by AFF_1:24;
A18: a9,b9 // b,a by A11,AFF_1:4;
A19: c in M by A16,AFF_1:24;
A20: a in A by A3,A6,AFF_1:24;
A21: A is being_line by A3,A6,AFF_1:24;
then
A22: a9 in A by A3,A6,A9,A14,A20,AFF_1:25;
A23: o<>b by A3,A6,A13,AFF_1:35;
then
A24: P is being_line by AFF_1:24;
A25: b in P by A23,AFF_1:24;
A26: A<>P
proof
assume A=P;
then a,b // A by A21,A20,A25,AFF_1:40,41;
hence contradiction by A3,A6,A8,A13,A14,A20,AFF_1:45,53;
end;
A27: o in P by A23,AFF_1:24;
then
A28: b9 in P by A10,A23,A24,A25,AFF_1:25;
A29: a9<>b9
proof
A30: a9,c9 // c,a by A12,AFF_1:4;
assume
A31: a9=b9;
then a9 in K by A3,A21,A24,A14,A27,A22,A28,A26,AFF_1:18;
then a9=c9 by A2,A4,A5,A6,A30,AFF_1:48;
hence contradiction by A15,A31,AFF_1:3;
end;
A32: a9<>c9
proof
assume a9=c9;
then
A33: a9 in P by A2,A3,A5,A6,A21,A14,A20,A27,A22,AFF_1:18;
a9,b9 // b,a by A11,AFF_1:4;
then a in P by A24,A25,A28,A29,A33,AFF_1:48;
hence contradiction by A3,A6,A24,A27,A26,AFF_1:24;
end;
then
A34: T is being_line & c9 in T by AFF_1:24;
A35: M is being_line by A16,AFF_1:24;
then consider N such that
A36: b9 in N and
A37: M // N by AFF_1:49;
A38: N is being_line by A37,AFF_1:36;
A39: not LIN a,b,c
proof
assume LIN a,b,c;
then a,b // a,c by AFF_1:def 1;
then a,c // K by A8,A13,AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2,A4,A6,AFF_1:23;
end;
not a9,c9 // N
proof
assume
A40: a9,c9 // N;
a9,c9 // a,c by A12,AFF_1:4;
then a,c // N by A32,A40,AFF_1:32;
then a,c // M by A37,AFF_1:43;
then c,a // M by AFF_1:34;
then a in M by A35,A19,AFF_1:23;
hence contradiction by A39,A35,A17,A19,AFF_1:21;
end;
then consider x such that
A41: x in N and
A42: LIN a9,c9,x by A38,AFF_1:59;
A43: b,c // b9,x by A17,A19,A36,A37,A41,AFF_1:39;
a9,c9 // a9,x by A42,AFF_1:def 1;
then a,c // a9,x by A12,A32,AFF_1:5;
then
A44: x in K by A1,A2,A3,A4,A6,A7,A8,A9,A10,A11,A13,A43;
A45: a9 in T by A32,AFF_1:24;
then x in T by A32,A34,A42,AFF_1:25;
then K=T by A2,A5,A15,A34,A43,A44,AFF_1:18;
then a9 in P by A2,A3,A6,A21,A14,A20,A27,A22,A45,AFF_1:18;
then a in P by A24,A25,A28,A29,A18,AFF_1:48;
hence contradiction by A3,A6,A24,A27,A26,AFF_1:24;
end;
theorem Th7:
AP is translational iff AP is satisfying_des_1
proof
hereby assume
A1: AP is translational;
thus AP is satisfying_des_1
proof
let A,P,C,a,b,c,a9,b9,c9;
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: c in C & c9 in C and
A8: A is being_line and
A9: P is being_line and
A10: C is being_line and
A11: A<>P and
A12: A<>C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9 and
A15: b,c // b9,c9 and
A16: not LIN a,b,c and
A17: c <>c9;
assume
A18: not A // C;
consider K such that
A19: c9 in K and
A20: A // K by A8,AFF_1:49;
A21: a<>c by A16,AFF_1:7;
A22: not a,c // K
proof
assume a,c // K;
then a,c // A by A20,AFF_1:43;
then
A23: c in A by A3,A8,AFF_1:23;
a9,c9 // a,c by A14,AFF_1:4;
then a9,c9 // A by A3,A8,A21,A23,AFF_1:27;
then c9 in A by A4,A8,AFF_1:23;
hence contradiction by A7,A8,A10,A12,A17,A23,AFF_1:18;
end;
A24: A<>K
proof
assume
A25: A=K;
a9,c9 // a,c by A14,AFF_1:4;
then a9=c9 by A4,A19,A20,A22,A25,AFF_1:32,40;
then a9,b9 // b,c by A15,AFF_1:4;
then a9=b9 or a,b // b,c by A13,AFF_1:5;
then b9 in A or b,a // b,c by A4,AFF_1:4;
then LIN b,a,c by A2,A6,A11,AFF_1:45,def 1;
hence contradiction by A16,AFF_1:6;
end;
A26: now
assume b9=c9;
then a,b // a,c or a9=b9 by A13,A14,AFF_1:5;
hence contradiction by A2,A4,A6,A11,A16,AFF_1:45,def 1;
end;
A27: K is being_line by A20,AFF_1:36;
then consider x such that
A28: x in K and
A29: LIN a,c,x by A22,AFF_1:59;
a,c // a,x by A29,AFF_1:def 1;
then a,x // a9,c9 by A14,A21,AFF_1:5;
then b,x // b9,c9 by A1,A2,A3,A4,A5,A6,A8,A9,A11,A13,A19,A20,A27,A28,A24;
then b,x // b,c or b9=c9 by A15,AFF_1:5;
then LIN b,x,c by A26,AFF_1:def 1;
then
A30: LIN x,c,b by AFF_1:6;
A31: LIN x,c, c by AFF_1:7;
LIN x,c,a by A29,AFF_1:6;
then c in K by A16,A28,A30,A31,AFF_1:8;
hence contradiction by A7,A10,A17,A18,A19,A20,A27,AFF_1:18;
end;
end;
assume
A32: AP is satisfying_des_1;
let A,P,C,a,b,c,a9,b9,c9;
assume that
A33: A // P and
A34: A // C and
A35: a in A and
A36: a9 in A and
A37: b in P and
A38: b9 in P and
A39: c in C and
A40: c9 in C and
A41: A is being_line and
A42: P is being_line and
A43: C is being_line and
A44: A<>P and
A45: A<>C and
A46: a,b // a9,b9 and
A47: a,c // a9,c9;
A48: a<>b by A33,A35,A37,A44,AFF_1:45;
A49: a9<>b9 by A33,A36,A38,A44,AFF_1:45;
set K=Line(a,c), N=Line(b9,c9);
A50: a<>c by A34,A35,A39,A45,AFF_1:45;
then
A51: a in K by AFF_1:24;
assume
A52: not b,c // b9,c9;
then
A53: b9<>c9 by AFF_1:3;
then
A54: b9 in N by AFF_1:24;
A55: b<>c by A52,AFF_1:3;
A56: not LIN a,b,c
proof
assume
A57: LIN a,b,c;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A58: b,c // a9,b9 by A46,A48,AFF_1:5;
LIN c,b,a by A57,AFF_1:6;
then c,b // c,a by AFF_1:def 1;
then b,c // a,c by AFF_1:4;
then b,c // a9,c9 by A47,A50,AFF_1:5;
then a9,c9 // a9,b9 by A55,A58,AFF_1:5;
then LIN a9,c9,b9 by AFF_1:def 1;
then LIN b9,c9,a9 by AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A52,A49,A58,AFF_1:5;
end;
A59: c in K by A50,AFF_1:24;
A60: N is being_line by A53,AFF_1:24;
then consider M such that
A61: b in M and
A62: N // M by AFF_1:49;
A63: c9 in N by A53,AFF_1:24;
A64: a9<>c9 by A34,A36,A40,A45,AFF_1:45;
A65: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b // a9,c9 by A46,A49,AFF_1:5;
then a,b // a,c by A47,A64,AFF_1:5;
hence contradiction by A56,AFF_1:def 1;
end;
A66: not K // M
proof
assume K // M;
then K // N by A62,AFF_1:44;
then a,c // b9,c9 by A51,A59,A54,A63,AFF_1:39;
then a9,c9 // b9,c9 by A47,A50,AFF_1:5;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def 1;
hence contradiction by A65,AFF_1:6;
end;
A67: K is being_line by A50,AFF_1:24;
A68: M is being_line by A62,AFF_1:36;
then consider x such that
A69: x in K and
A70: x in M by A67,A66,AFF_1:58;
A71: b,x // b9,c9 by A54,A63,A61,A62,A70,AFF_1:39;
set D=Line(x,c9);
A72: A<>D
proof
assume A=D;
then c9 in A by AFF_1:15;
hence contradiction by A34,A40,A45,AFF_1:45;
end;
A73: x in D by AFF_1:15;
LIN a,c,x by A67,A51,A59,A69,AFF_1:21;
then a,c // a,x by AFF_1:def 1;
then
A74: a,x // a9,c9 by A47,A50,AFF_1:5;
A75: c9 in D by AFF_1:15;
A76: not LIN a,b,x
proof
A77: a<>x
proof
assume a=x;
then a,b // b9,c9 by A54,A63,A61,A62,A70,AFF_1:39;
then a9,b9 // b9,c9 by A46,A48,AFF_1:5;
then b9,a9 // b9,c9 by AFF_1:4;
then LIN b9,a9,c9 by AFF_1:def 1;
hence contradiction by A65,AFF_1:6;
end;
assume LIN a,b,x;
then LIN x,b,a by AFF_1:6;
then
A78: x,b // x,a by AFF_1:def 1;
x<>b by A67,A51,A59,A56,A69,AFF_1:21;
hence contradiction by A67,A51,A61,A68,A66,A69,A70,A78,A77,AFF_1:38;
end;
A79: P // C by A33,A34,AFF_1:44;
A80: x<>c9
proof
A81: now
A82: P // P by A33,AFF_1:44;
assume
A83: P=N;
then c in P by A39,A40,A79,A63,AFF_1:45;
hence contradiction by A37,A38,A52,A63,A83,A82,AFF_1:39;
end;
assume x=c9;
then M=N by A63,A62,A70,AFF_1:45;
then
A84: P=N or b=b9 by A37,A38,A42,A60,A54,A61,AFF_1:18;
then b,a // b,a9 by A46,A81,AFF_1:4;
then LIN b,a,a9 by AFF_1:def 1;
then LIN a,a9,b by AFF_1:6;
then b in A or a=a9 by A35,A36,A41,AFF_1:25;
then LIN a9,c,c9 by A33,A37,A44,A47,AFF_1:45,def 1;
then LIN c,c9,a9 by AFF_1:6;
then c =c9 or a9 in C by A39,A40,A43,AFF_1:25;
hence contradiction by A34,A36,A45,A52,A84,A81,AFF_1:2,45;
end;
then D is being_line by AFF_1:24;
then A // D by A32,A33,A35,A36,A37,A38,A41,A42,A44,A46,A71,A74,A73,A75
,A80,A76,A72;
then D // C by A34,AFF_1:44;
then C=D by A40,A75,AFF_1:45;
then C=K by A39,A43,A52,A67,A59,A69,A71,A73,AFF_1:18;
hence contradiction by A34,A35,A45,A51,AFF_1:45;
end;
theorem
AP is satisfying_pap iff AP is satisfying_pap_1
proof
hereby assume
A1: AP is satisfying_pap;
thus AP is satisfying_pap_1
proof
let M,N,a,b,c,a9,b9,c9;
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M<>N and
A9: a9 in N and
A10: b9 in N and
A11: a,b9 // b,a9 and
A12: b,c9 // c,b9 and
A13: a,c9 // c,a9 and
A14: a9<>b9;
A15: c <>a9 by A6,A7,A8,A9,AFF_1:45;
set C=Line(c,b9);
A16: c <>b9 by A6,A7,A8,A10,AFF_1:45;
then C is being_line by AFF_1:24;
then consider K such that
A17: b in K and
A18: C // K by AFF_1:49;
A19: c in C & b9 in C by A16,AFF_1:24;
A20: not K // N
proof
assume K // N;
then C // N by A18,AFF_1:44;
then C // M by A7,AFF_1:44;
then b9 in M by A6,A19,AFF_1:45;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
K is being_line by A18,AFF_1:36;
then consider x such that
A21: x in K and
A22: x in N by A3,A20,AFF_1:58;
A23: b,x // c,b9 by A19,A17,A18,A21,AFF_1:39;
then a,x // c,a9 by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A22;
then a,x // a,c9 by A13,A15,AFF_1:5;
then LIN a,x,c9 by AFF_1:def 1;
then
A24: LIN c9,x,a by AFF_1:6;
A25: a<>b
proof
assume a=b;
then LIN a,b9,a9 by A11,AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then a9=b9 or a in N by A3,A9,A10,AFF_1:25;
hence contradiction by A4,A7,A8,A14,AFF_1:45;
end;
A26: c9<>b
proof
assume c9=b;
then a9 in M by A2,A4,A5,A6,A13,A25,AFF_1:48;
hence contradiction by A7,A8,A9,AFF_1:45;
end;
b,x // b,c9 by A12,A16,A23,AFF_1:5;
then LIN b,x,c9 by AFF_1:def 1;
then
A27: LIN c9,x,b by AFF_1:6;
assume
A28: not c9 in N;
LIN c9,x,c9 by AFF_1:7;
then c9 in M by A2,A4,A5,A28,A25,A22,A24,A27,AFF_1:8,25;
then b9 in M by A2,A5,A6,A12,A26,AFF_1:48;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
end;
assume
A29: AP is satisfying_pap_1;
let M,N,a,b,c,a9,b9,c9;
assume that
A30: M is being_line and
A31: N is being_line and
A32: a in M and
A33: b in M and
A34: c in M and
A35: M // N & M<>N and
A36: a9 in N and
A37: b9 in N and
A38: c9 in N and
A39: a,b9 // b,a9 and
A40: b,c9 // c,b9;
set A=Line(c,a9), D=Line(b,c9);
A41: b<>c9 by A33,A35,A38,AFF_1:45;
then
A42: b in D & c9 in D by AFF_1:24;
assume
A43: not a,c9 // c,a9;
then
A44: c <>a9 by AFF_1:3;
then
A45: c in A by AFF_1:24;
A46: a9 in A by A44,AFF_1:24;
A47: A is being_line by A44,AFF_1:24;
then consider P such that
A48: a in P and
A49: A // P by AFF_1:49;
A50: a9<>b9
proof
assume
A51: a9=b9;
then a9,a // a9,b by A39,AFF_1:4;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:6;
then a=b or a9 in M by A30,A32,A33,AFF_1:25;
hence contradiction by A35,A36,A40,A43,A51,AFF_1:45;
end;
A52: not D // P
proof
assume D // P;
then c,b9 // P by A40,A41,A42,AFF_1:32,40;
then c,b9 // A by A49,AFF_1:43;
then b9 in A by A47,A45,AFF_1:23;
then c in N by A31,A36,A37,A50,A47,A45,A46,AFF_1:18;
hence contradiction by A34,A35,AFF_1:45;
end;
A53: D is being_line by A41,AFF_1:24;
P is being_line by A49,AFF_1:36;
then consider x such that
A54: x in D and
A55: x in P by A53,A52,AFF_1:58;
LIN b,x,c9 by A53,A42,A54,AFF_1:21;
then b,x // b,c9 by AFF_1:def 1;
then
A56: b,x // c,b9 by A40,A41,AFF_1:5;
a,x // c,a9 by A45,A46,A48,A49,A55,AFF_1:39;
then x in N by A29,A30,A31,A32,A33,A34,A35,A36,A37,A39,A50,A56;
then x=c9 or b in N by A31,A38,A53,A42,A54,AFF_1:18;
hence contradiction by A33,A35,A43,A45,A46,A48,A49,A55,AFF_1:39,45;
end;
theorem Th9:
AP is Pappian implies AP is satisfying_pap
proof
assume
A1: AP is Pappian;
let M,N,a,b,c,a9,b9,c9;
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M<>N and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9;
A14: b<>a9 by A5,A7,A8,A9,AFF_1:45;
set K=Line(a,c9), C=Line(c,b9);
A15: c <>b9 by A6,A7,A8,A10,AFF_1:45;
then
A16: C is being_line by AFF_1:24;
assume
A17: not a,c9 // c,a9;
A18: now
assume
A19: a=b;
then LIN a,b9,a9 by A12,AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then a9=b9 or a in N by A3,A9,A10,AFF_1:25;
hence contradiction by A4,A7,A8,A13,A17,A19,AFF_1:45;
end;
A20: now
assume a9=b9;
then a9,a // a9,b by A12,AFF_1:4;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:6;
then a9 in M by A2,A4,A5,A18,AFF_1:25;
hence contradiction by A7,A8,A9,AFF_1:45;
end;
A21: now
assume
A22: b=c;
then LIN b,c9,b9 by A13,AFF_1:def 1;
then LIN b9,c9,b by AFF_1:6;
then b9=c9 or b in N by A3,A10,A11,AFF_1:25;
hence contradiction by A5,A7,A8,A12,A17,A22,AFF_1:45;
end;
A23: now
assume b9=c9;
then b9,b // b9,c by A13,AFF_1:4;
then LIN b9,b,c by AFF_1:def 1;
then LIN b,c,b9 by AFF_1:6;
then b9 in M by A2,A5,A6,A21,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
A24: a<>c9 by A4,A7,A8,A11,AFF_1:45;
then
A25: a in K by AFF_1:24;
K is being_line by A24,AFF_1:24;
then consider T such that
A26: a9 in T and
A27: K // T by AFF_1:49;
A28: T is being_line by A27,AFF_1:36;
A29: c9 in K by A24,AFF_1:24;
A30: c in C & b9 in C by A15,AFF_1:24;
not C // T
proof
assume C // T;
then C // K by A27,AFF_1:44;
then c,b9 // a,c9 by A25,A29,A30,AFF_1:39;
then b,c9 // a,c9 by A13,A15,AFF_1:5;
then c9,b // c9,a by AFF_1:4;
then LIN c9,b,a by AFF_1:def 1;
then LIN a,b,c9 by AFF_1:6;
then c9 in M by A2,A4,A5,A18,AFF_1:25;
hence contradiction by A7,A8,A11,AFF_1:45;
end;
then consider x such that
A31: x in C and
A32: x in T by A16,A28,AFF_1:58;
set D=Line(x,b);
A33: x<>b
proof
assume x=b;
then LIN b,c,b9 by A16,A30,A31,AFF_1:21;
then b9 in M by A2,A5,A6,A21,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
then
A34: b in D by AFF_1:24;
then
A35: D<>N by A5,A7,A8,AFF_1:45;
A36: D is being_line by A33,AFF_1:24;
A37: x in D by A33,AFF_1:24;
not D // N
proof
assume D // N;
then D // M by A7,AFF_1:44;
then x in M by A5,A37,A34,AFF_1:45;
then c in T or b9 in M by A2,A6,A16,A30,A31,A32,AFF_1:18;
hence contradiction by A7,A8,A10,A17,A25,A29,A26,A27,AFF_1:39,45;
end;
then consider o such that
A38: o in D and
A39: o in N by A3,A36,AFF_1:58;
LIN b9,c,x by A16,A30,A31,AFF_1:21;
then
A40: b9,c // b9,x by AFF_1:def 1;
A41: a9<>x
proof
assume a9=x;
then b9,a9 // b9,c by A40,AFF_1:4;
then LIN b9,a9,c by AFF_1:def 1;
then c in N by A3,A9,A10,A20,AFF_1:25;
hence contradiction by A6,A7,A8,AFF_1:45;
end;
A42: now
assume o=x;
then N=T by A3,A9,A26,A28,A32,A39,A41,AFF_1:18;
then N=K by A11,A29,A27,AFF_1:45;
hence contradiction by A4,A7,A8,A25,AFF_1:45;
end;
A43: a,c9 // x,a9 by A25,A29,A26,A27,A32,AFF_1:39;
A44: now
assume o=a9;
then LIN a9,b,x by A36,A37,A34,A38,AFF_1:21;
then a9,b // a9,x by AFF_1:def 1;
then b,a9 // x,a9 by AFF_1:4;
then a,b9 // x,a9 by A12,A14,AFF_1:5;
then a,b9 // a,c9 by A43,A41,AFF_1:5;
then LIN a,b9,c9 by AFF_1:def 1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A3,A10,A11,A23,AFF_1:25;
hence contradiction by A4,A7,A8,AFF_1:45;
end;
c,b9 // x,b9 by A40,AFF_1:4;
then
A45: b,c9 // x,b9 by A13,A15,AFF_1:5;
A46: a<>b9 by A4,A7,A8,A10,AFF_1:45;
not a,b9 // D
proof
assume a,b9 // D;
then b,a9 // D by A12,A46,AFF_1:32;
then a9 in D by A36,A34,AFF_1:23;
then b in T by A26,A28,A32,A36,A37,A34,A41,AFF_1:18;
then b,a9 // a,c9 by A25,A29,A26,A27,AFF_1:39;
then a,b9 // a,c9 by A12,A14,AFF_1:5;
then LIN a,b9,c9 by AFF_1:def 1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A3,A10,A11,A23,AFF_1:25;
hence contradiction by A4,A7,A8,AFF_1:45;
end;
then consider y such that
A47: y in D and
A48: LIN a,b9,y by A36,AFF_1:59;
A49: LIN a,y,a by AFF_1:7;
A50: b9<>x
proof
assume b9=x;
then a,c9 // a9,b9 by A25,A29,A26,A27,A32,AFF_1:39;
then a,c9 // N by A3,A9,A10,A20,AFF_1:27;
then c9,a // N by AFF_1:34;
then a in N by A3,A11,AFF_1:23;
hence contradiction by A4,A7,A8,AFF_1:45;
end;
A51: now
assume o=b9;
then LIN b9,x,b by A36,A37,A34,A38,AFF_1:21;
then b9,x // b9,b by AFF_1:def 1;
then x,b9 // b,b9 by AFF_1:4;
then b,c9 // b,b9 by A45,A50,AFF_1:5;
then LIN b,c9,b9 by AFF_1:def 1;
then LIN b9,c9,b by AFF_1:6;
then b in N by A3,A10,A11,A23,AFF_1:25;
hence contradiction by A5,A7,A8,AFF_1:45;
end;
A52: now
assume o=y;
then LIN b9,o,a by A48,AFF_1:6;
then a in N by A3,A10,A39,A51,AFF_1:25;
hence contradiction by A4,A7,A8,AFF_1:45;
end;
A53: b<>c9 by A5,A7,A8,A11,AFF_1:45;
A54: now
assume o=c9;
then D // C by A13,A15,A53,A16,A30,A36,A34,A38,AFF_1:38;
then b in C by A31,A37,A34,AFF_1:45;
then LIN c,b,b9 by A16,A30,AFF_1:21;
then b9 in M by A2,A5,A6,A21,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
LIN b9,a,y by A48,AFF_1:6;
then b9,a // b9,y by AFF_1:def 1;
then a,b9 // y,b9 by AFF_1:4;
then
A55: y,b9 // b,a9 by A12,A46,AFF_1:5;
o<>b by A5,A7,A8,A39,AFF_1:45;
then y,c9 // x,a9 by A1,A3,A9,A10,A11,A36,A37,A34,A38,A39,A45,A47,A55,A35
,A51,A44,A54,A42,A52;
then y,c9 // a,c9 by A43,A41,AFF_1:5;
then c9,y // c9,a by AFF_1:4;
then LIN c9,y,a by AFF_1:def 1;
then
A56: LIN a,y,c9 by AFF_1:6;
LIN a,y,b9 by A48,AFF_1:6;
then a in D or a in N by A3,A10,A11,A23,A47,A56,A49,AFF_1:8,25;
then D // N by A2,A4,A5,A7,A8,A18,A36,A34,AFF_1:18,45;
hence contradiction by A38,A39,A35,AFF_1:45;
end;
theorem Th10:
AP is satisfying_PPAP iff AP is Pappian & AP is satisfying_pap
proof
A1: AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP
proof
assume that
A2: AP is Pappian and
A3: AP is satisfying_pap;
thus AP is satisfying_PPAP
proof
let M,N,a,b,c,a9,b9,c9;
assume that
A4: M is being_line and
A5: N is being_line and
A6: a in M and
A7: b in M and
A8: c in M and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9;
now
assume
A14: M<>N;
assume
A15: not thesis;
now
assume not M // N;
then consider o such that
A16: o in M and
A17: o in N by A4,A5,AFF_1:58;
A18: o<>a
proof
assume
A19: o=a;
then o,b9 // a9,b by A12,AFF_1:4;
then o=b9 or b in N by A5,A9,A10,A17,AFF_1:48;
then o=b9 or o=b by A4,A5,A7,A14,A16,A17,AFF_1:18;
then c,o // b,c9 or o,c9 // b9,c by A13,AFF_1:4;
then c9 in M or c =o or c in N or o=c9 by A4,A5,A7,A8,A10,A11,A16
,A17,AFF_1:48;
then o=c or o=c9 by A4,A5,A8,A11,A14,A16,A17,AFF_1:18;
hence contradiction by A5,A9,A11,A15,A17,A19,AFF_1:3,51;
end;
A20: o<>b
proof
assume
A21: o=b;
then o,c9 // b9,c by A13,AFF_1:4;
then o=c9 or c in N by A5,A10,A11,A17,AFF_1:48;
then
A22: o=c9 or o=c by A4,A5,A8,A14,A16,A17,AFF_1:18;
o,a9 // b9,a by A12,A21,AFF_1:4;
then o=a9 or a in N by A5,A9,A10,A17,AFF_1:48;
hence contradiction by A4,A5,A6,A8,A14,A15,A16,A17,A18,A22,AFF_1:3
,18,51;
end;
A23: o<>c9
proof
assume
A24: o=c9;
then b9 in M by A4,A7,A8,A13,A16,A20,AFF_1:48;
then a,o // b,a9 by A4,A5,A10,A12,A14,A16,A17,AFF_1:18;
then a9 in M by A4,A6,A7,A16,A18,AFF_1:48;
hence contradiction by A4,A6,A8,A15,A16,A24,AFF_1:51;
end;
A25: o<>c
proof
assume
A26: o=c;
then o,b9 // c9,b by A13,AFF_1:4;
then o=b9 or b in N by A5,A10,A11,A17,AFF_1:48;
then a9 in M by A4,A5,A6,A7,A9,A12,A16,A17,A18,A20,AFF_1:18,48;
then a9=o by A4,A5,A9,A14,A16,A17,AFF_1:18;
hence contradiction by A15,A26,AFF_1:3;
end;
A27: o<>a9
proof
assume
A28: o=a9;
then o,b // a,b9 by A12,AFF_1:4;
then b9 in M by A4,A6,A7,A16,A20,AFF_1:48;
then o=b9 by A4,A5,A10,A14,A16,A17,AFF_1:18;
then c,o // b,c9 by A13,AFF_1:4;
then c9 in M by A4,A7,A8,A16,A25,AFF_1:48;
hence contradiction by A4,A6,A8,A15,A16,A28,AFF_1:51;
end;
o<>b9
proof
assume
A29: o=b9;
then o,c // b,c9 by A13,AFF_1:4;
then
A30: c9 in M by A4,A7,A8,A16,A25,AFF_1:48;
a9 in M by A4,A6,A7,A12,A16,A18,A29,AFF_1:48;
hence contradiction by A4,A6,A8,A15,A30,AFF_1:51;
end;
hence thesis by A2,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A16,A17,A18
,A20,A25,A27,A23;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14;
end;
hence thesis by A4,A6,A8,A9,A11,AFF_1:51;
end;
end;
thus thesis by A1;
end;
theorem
AP is Pappian implies AP is Desarguesian
proof
assume
A1: AP is Pappian;
then AP is satisfying_pap by Th9;
then
A2: AP is satisfying_PPAP by A1,Th10;
let A,P,C,o,a,b,c,a9,b9,c9;
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o<>a and
A7: o<>b and
o<>c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A<>P and
A18: A<>C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9;
assume
A21: not b,c // b9,c9;
then
A22: b<>c by AFF_1:3;
A23: a<>c by A3,A5,A6,A8,A12,A14,A16,A18,AFF_1:18;
A24: not b in C
proof
assume
A25: b in C;
then b9 in C by A4,A5,A7,A10,A11,A15,A16,AFF_1:18;
hence contradiction by A12,A13,A16,A21,A25,AFF_1:51;
end;
A26: a<>b by A3,A4,A6,A8,A10,A14,A15,A17,AFF_1:18;
A27: a<>a9
proof
assume
A28: a=a9;
then LIN a,c,c9 by A20,AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then
A29: c =c9 or a in C by A12,A13,A16,AFF_1:25;
LIN a,b,b9 by A19,A28,AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b=b9 or a in P by A10,A11,A15,AFF_1:25;
hence contradiction by A3,A4,A5,A6,A8,A14,A15,A16,A17,A18,A21,A29,AFF_1:2
,18;
end;
set M=Line(b9,c9), N=Line(a9,b9), D=Line(a9,c9);
A30: a9<>b9
proof
A31: a9,c9 // c,a by A20,AFF_1:4;
assume
A32: a9=b9;
then a9 in C by A3,A4,A5,A9,A11,A14,A15,A17,AFF_1:18;
then a in C or a9=c9 by A12,A13,A16,A31,AFF_1:48;
hence contradiction by A3,A5,A6,A8,A14,A16,A18,A21,A32,AFF_1:3,18;
end;
then
A33: N is being_line by AFF_1:24;
A34: a9<>c9
proof
assume a9=c9;
then
A35: a9 in P by A3,A4,A5,A9,A13,A14,A16,A18,AFF_1:18;
a9,b9 // b,a by A19,AFF_1:4;
then a in P by A10,A11,A15,A30,A35,AFF_1:48;
hence contradiction by A3,A4,A6,A8,A14,A15,A17,AFF_1:18;
end;
A36: not LIN a9,b9,c9
proof
assume
A37: LIN a9,b9,c9;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A20,A34,AFF_1:5;
then a,b // a,c by A19,A30,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A38: b,c // a9,b9 by A19,A26,AFF_1:5;
LIN b9,c9,a9 by A37,AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A21,A30,A38,AFF_1:5;
end;
A39: not LIN a,b,c
proof
assume LIN a,b,c;
then a,b // a,c by AFF_1:def 1;
then a,b // a9,c9 by A20,A23,AFF_1:5;
then a9,b9 // a9,c9 by A19,A26,AFF_1:5;
hence contradiction by A36,AFF_1:def 1;
end;
A40: now
LIN o,a,a9 by A3,A8,A9,A14,AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
then
A41: a9,o // a,o by AFF_1:4;
set M=Line(b,c), N=Line(a,b), D=Line(a,c);
A42: N is being_line by A26,AFF_1:24;
M is being_line by A22,AFF_1:24;
then consider K such that
A43: o in K and
A44: M // K by AFF_1:49;
A45: K is being_line by A44,AFF_1:36;
A46: a in N by A26,AFF_1:24;
A47: b in N by A26,AFF_1:24;
A48: b in M & c in M by A22,AFF_1:24;
not N // K
proof
assume N // K;
then N // M by A44,AFF_1:44;
then c in N by A48,A47,AFF_1:45;
hence contradiction by A39,A42,A46,A47,AFF_1:21;
end;
then consider p such that
A49: p in N and
A50: p in K by A42,A45,AFF_1:58;
A51: b,c // p,o by A48,A43,A44,A50,AFF_1:39;
A52: o<>p
proof
assume o=p;
then LIN o,a,b by A42,A46,A47,A49,AFF_1:21;
then b in A by A3,A6,A8,A14,AFF_1:25;
hence contradiction by A3,A4,A7,A10,A14,A15,A17,AFF_1:18;
end;
set R=Line(a9,p);
A53: p<>a9
proof
assume p=a9;
then b in A by A8,A9,A14,A27,A42,A46,A47,A49,AFF_1:18;
hence contradiction by A3,A4,A7,A10,A14,A15,A17,AFF_1:18;
end;
then
A54: R is being_line by AFF_1:24;
D is being_line by A23,AFF_1:24;
then consider T such that
A55: p in T and
A56: D // T by AFF_1:49;
A57: a in D & c in D by A23,AFF_1:24;
A58: not C // T
proof
assume C // T;
then C // D by A56,AFF_1:44;
then a in C by A12,A57,AFF_1:45;
hence contradiction by A3,A5,A6,A8,A14,A16,A18,AFF_1:18;
end;
T is being_line by A56,AFF_1:36;
then consider q such that
A59: q in C and
A60: q in T by A16,A58,AFF_1:58;
A61: p,q // a,c by A57,A55,A56,A60,AFF_1:39;
then
A62: b,q // a,o by A2,A5,A12,A16,A42,A46,A47,A49,A59,A51;
A63: a9 in R & p in R by A53,AFF_1:24;
assume not b,c // A;
then
A64: K<>A by A48,A44,AFF_1:40;
not b,q // R
proof
assume b,q // R;
then
A65: a,o // R by A24,A59,A62,AFF_1:32;
a,o // A by A3,A8,A14,AFF_1:40,41;
then p in A by A6,A9,A63,A65,AFF_1:45,53;
hence contradiction by A3,A14,A43,A45,A50,A52,A64,AFF_1:18;
end;
then consider r such that
A66: r in R and
A67: LIN b,q,r by A54,AFF_1:59;
A68: now
assume r=q;
then b,r // a,o by A2,A5,A12,A16,A42,A46,A47,A49,A59,A51,A61;
then
A69: r,b // o,a by AFF_1:4;
LIN o,a,a9 by A3,A8,A9,A14,AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
hence r,b // o,a9 by A6,A69,AFF_1:5;
end;
LIN q,r,b by A67,AFF_1:6;
then q,r // q,b by AFF_1:def 1;
then r,q // b,q by AFF_1:4;
then r,q // a,o by A24,A59,A62,AFF_1:5;
then
A70: a9,o // r,q by A6,A41,AFF_1:5;
LIN b,a,p by A42,A46,A47,A49,AFF_1:21;
then b,a // b,p by AFF_1:def 1;
then a,b // p,b by AFF_1:4;
then
A71: p,b // a9,b9 by A19,A26,AFF_1:5;
LIN r,b,q by A67,AFF_1:6;
then r,b // r,q by AFF_1:def 1;
then a9,o // r,b by A70,A68,AFF_1:4,5;
then
A72: p,o // r,b9 by A2,A4,A10,A11,A15,A54,A63,A66,A71;
p,q // a9,c9 by A20,A23,A61,AFF_1:5;
then
A73: p,o // r,c9 by A2,A5,A13,A16,A59,A54,A63,A66,A70;
then r,c9 // r,b9 by A52,A72,AFF_1:5;
then LIN r,c9,b9 by AFF_1:def 1;
then LIN c9,b9,r by AFF_1:6;
then c9,b9 // c9,r by AFF_1:def 1;
then
A74: r,c9 // b9,c9 by AFF_1:4;
b,c // r,c9 by A52,A51,A73,AFF_1:5;
then r=c9 by A21,A74,AFF_1:5;
then p,o // b9,c9 by A72,AFF_1:4;
hence contradiction by A21,A52,A51,AFF_1:5;
end;
A75: b9 in N by A30,AFF_1:24;
A76: b9<>c9 by A21,AFF_1:3;
then
A77: b9 in M & c9 in M by AFF_1:24;
M is being_line by A76,AFF_1:24;
then consider K such that
A78: o in K and
A79: M // K by AFF_1:49;
A80: K is being_line by A79,AFF_1:36;
A81: a9 in N by A30,AFF_1:24;
not N // K
proof
assume N // K;
then N // M by A79,AFF_1:44;
then c9 in N by A77,A75,AFF_1:45;
hence contradiction by A36,A33,A81,A75,AFF_1:21;
end;
then consider p such that
A82: p in N and
A83: p in K by A33,A80,AFF_1:58;
A84: o<>a9
proof
assume
A85: o=a9;
a9,b9 // b,a by A19,AFF_1:4;
then a in P by A4,A10,A11,A15,A30,A85,AFF_1:48;
hence contradiction by A3,A4,A6,A8,A14,A15,A17,AFF_1:18;
end;
A86: o<>p
proof
assume o=p;
then LIN o,a9,b9 by A33,A81,A75,A82,AFF_1:21;
then
A87: b9 in A by A3,A9,A14,A84,AFF_1:25;
a9,b9 // a,b by A19,AFF_1:4;
then b in A by A8,A9,A14,A30,A87,AFF_1:48;
hence contradiction by A3,A4,A7,A10,A14,A15,A17,AFF_1:18;
end;
D is being_line by A34,AFF_1:24;
then consider T such that
A88: p in T and
A89: D // T by AFF_1:49;
A90: T is being_line by A89,AFF_1:36;
A91: a9 in D & c9 in D by A34,AFF_1:24;
not C // T
proof
assume C // T;
then C // D by A89,AFF_1:44;
then a9 in C by A13,A91,AFF_1:45;
hence contradiction by A3,A5,A9,A14,A16,A18,A84,AFF_1:18;
end;
then consider q such that
A92: q in C and
A93: q in T by A16,A90,AFF_1:58;
A94: b9,c9 // p,o by A77,A78,A79,A83,AFF_1:39;
A95: o<>b9
proof
assume
A96: o=b9;
b9,a9 // a,b by A19,AFF_1:4;
then b in A by A3,A8,A9,A14,A30,A96,AFF_1:48;
hence contradiction by A3,A4,A7,A10,A14,A15,A17,AFF_1:18;
end;
A97: b9<>q
proof
assume b9=q;
then P=C by A4,A5,A11,A15,A16,A95,A92,AFF_1:18;
hence contradiction by A10,A11,A12,A13,A15,A21,AFF_1:51;
end;
set R=Line(a,p);
A98: p<>a
proof
assume p=a;
then b9 in A by A8,A9,A14,A27,A33,A81,A75,A82,AFF_1:18;
hence contradiction by A3,A4,A11,A14,A15,A17,A95,AFF_1:18;
end;
then
A99: R is being_line by AFF_1:24;
A100: p,q // a9,c9 by A91,A88,A89,A93,AFF_1:39;
then
A101: b9,q // a9,o by A2,A5,A13,A16,A33,A81,A75,A82,A92,A94;
A102: a in R & p in R by A98,AFF_1:24;
not b9,c9 // A by A14,A21,A40,AFF_1:31;
then
A103: K<>A by A77,A79,AFF_1:40;
not b9,q // R
proof
assume b9,q // R;
then
A104: a9,o // R by A101,A97,AFF_1:32;
a9,o // A by A3,A9,A14,AFF_1:40,41;
then p in A by A8,A84,A102,A104,AFF_1:45,53;
hence contradiction by A3,A14,A78,A80,A83,A86,A103,AFF_1:18;
end;
then consider r such that
A105: r in R and
A106: LIN b9,q,r by A99,AFF_1:59;
A107: now
assume r=q;
then b9,r // a9,o by A2,A5,A13,A16,A33,A81,A75,A82,A92,A94,A100;
then
A108: r,b9 // o,a9 by AFF_1:4;
LIN o,a9,a by A3,A8,A9,A14,AFF_1:21;
then o,a9 // o,a by AFF_1:def 1;
hence r,b9 // o,a by A84,A108,AFF_1:5;
end;
LIN b9,a9,p by A33,A81,A75,A82,AFF_1:21;
then b9,a9 // b9,p by AFF_1:def 1;
then p,b9 // a9,b9 by AFF_1:4;
then
A109: p,b9 // a,b by A19,A30,AFF_1:5;
LIN o,a,a9 by A3,A8,A9,A14,AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
then
A110: a,o // a9,o by AFF_1:4;
LIN q,r,b9 by A106,AFF_1:6;
then q,r // q,b9 by AFF_1:def 1;
then r,q // b9,q by AFF_1:4;
then r,q // a9,o by A101,A97,AFF_1:5;
then
A111: a,o // r,q by A84,A110,AFF_1:5;
LIN r,b9,q by A106,AFF_1:6;
then r,b9 // r,q by AFF_1:def 1;
then a,o // r,b9 by A111,A107,AFF_1:4,5;
then
A112: p,o // r,b by A2,A4,A10,A11,A15,A99,A102,A105,A109;
p,q // a,c by A20,A34,A100,AFF_1:5;
then
A113: p,o // r,c by A2,A5,A12,A16,A92,A99,A102,A105,A111;
then r,c // r,b by A86,A112,AFF_1:5;
then LIN r,c,b by AFF_1:def 1;
then LIN c,b,r by AFF_1:6;
then c,b // c,r by AFF_1:def 1;
then
A114: b,c // r,c by AFF_1:4;
b9,c9 // r,c by A86,A94,A113,AFF_1:5;
then r=c by A21,A114,AFF_1:5;
then b,c // p,o by A112,AFF_1:4;
hence contradiction by A21,A86,A94,AFF_1:5;
end;
theorem
AP is Desarguesian implies AP is Moufangian
proof
assume
A1: AP is Desarguesian;
let K,o,a,b,c,a9,b9,c9;
assume that
A2: K is being_line and
A3: o in K and
A4: c in K & c9 in K and
A5: not a in K and
A6: o<>c and
A7: a<>b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: a,b // a9,b9 & a,c // a9,c9 and
A11: a,b // K;
set A=Line(o,a), P=Line(o,b);
A12: o in A by A3,A5,AFF_1:24;
A13: now
assume
A14: o=b;
b,a // K by A11,AFF_1:34;
hence contradiction by A2,A3,A5,A14,AFF_1:23;
end;
then
A15: b in P by AFF_1:24;
A16: a in A by A3,A5,AFF_1:24;
A17: A is being_line by A3,A5,AFF_1:24;
A18: A<>P
proof
assume A=P;
then a,b // A by A17,A16,A15,AFF_1:40,41;
hence contradiction by A3,A5,A7,A11,A12,A16,AFF_1:45,53;
end;
A19: P is being_line & o in P by A13,AFF_1:24;
then
A20: b9 in P by A9,A13,A15,AFF_1:25;
a9 in A by A3,A5,A8,A17,A12,A16,AFF_1:25;
hence thesis by A1,A2,A3,A4,A5,A6,A10,A13,A17,A12,A16,A19,A15,A20,A18;
end;
theorem Th13:
AP is satisfying_TDES_1 implies AP is satisfying_des_1
proof
assume
A1: AP is satisfying_TDES_1;
let A,P,C,a,b,c,a9,b9,c9;
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: c in C and
A8: c9 in C and
A9: A is being_line and
A10: P is being_line and
A11: C is being_line and
A12: A<>P and
A13: A<>C and
A14: a,b // a9,b9 and
A15: a,c // a9,c9 and
A16: b,c // b9,c9 and
A17: not LIN a,b,c and
A18: c <>c9;
set P9=Line(a,b), C9=Line(a9,b9);
A19: a9<>b9 by A2,A4,A6,A12,AFF_1:45;
then
A20: a9 in C9 by AFF_1:24;
A21: a9<>c9
proof
assume a9=c9;
then b,c // a9,b9 by A16,AFF_1:4;
then a,b // b,c by A14,A19,AFF_1:5;
then b,a // b,c by AFF_1:4;
then LIN b,a,c by AFF_1:def 1;
hence contradiction by A17,AFF_1:6;
end;
A22: not c9 in A
proof
assume
A23: c9 in A;
a9,c9 // a,c by A15,AFF_1:4;
then c in A by A3,A4,A9,A21,A23,AFF_1:48;
hence contradiction by A7,A8,A9,A11,A13,A18,A23,AFF_1:18;
end;
A24: C9 is being_line by A19,AFF_1:24;
assume
A25: not A // C;
then consider o such that
A26: o in A and
A27: o in C by A9,A11,AFF_1:58;
A28: LIN o,c9,c by A7,A8,A11,A27,AFF_1:21;
A29: a<>a9
proof
assume
A30: a=a9;
then LIN a,c,c9 by A15,AFF_1:def 1;
then
A31: LIN c,c9,a by AFF_1:6;
LIN a,b,b9 by A14,A30,AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b=b9 or a in P by A5,A6,A10,AFF_1:25;
then LIN b,c,c9 by A2,A3,A12,A16,AFF_1:45,def 1;
then
A32: LIN c,c9,b by AFF_1:6;
LIN c,c9,c by AFF_1:7;
hence contradiction by A17,A18,A31,A32,AFF_1:8;
end;
A33: o<>a9
proof
assume
A34: o=a9;
a9,c9 // c,a by A15,AFF_1:4;
then a in C by A7,A8,A11,A27,A21,A34,AFF_1:48;
hence contradiction by A3,A4,A9,A11,A13,A27,A29,A34,AFF_1:18;
end;
A35: a<>b by A17,AFF_1:7;
then
A36: P9 is being_line by AFF_1:24;
consider N such that
A37: c9 in N and
A38: A // N by A9,AFF_1:49;
A39: b9 in C9 by A19,AFF_1:24;
A40: not N // C9
proof
assume N // C9;
then A // C9 by A38,AFF_1:44;
then b9 in A by A4,A39,A20,AFF_1:45;
hence contradiction by A2,A6,A12,AFF_1:45;
end;
N is being_line by A38,AFF_1:36;
then consider q such that
A41: q in N and
A42: q in C9 by A24,A40,AFF_1:58;
A43: c9,q // A by A37,A38,A41,AFF_1:40;
A44: c9<>q
proof
assume c9=q;
then LIN a9,b9,c9 by A24,A39,A20,A42,AFF_1:21;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A15,A21,AFF_1:5;
then a,b // a,c by A14,A19,AFF_1:5;
hence contradiction by A17,AFF_1:def 1;
end;
A45: c9,a9 // c,a by A15,AFF_1:4;
A46: c,b // c9,b9 by A16,AFF_1:4;
A47: a in P9 by A35,AFF_1:24;
A48: b<>c by A17,AFF_1:7;
A49: not c in P
proof
assume
A50: c in P;
then c9 in P by A5,A6,A10,A16,A48,AFF_1:48;
hence contradiction by A2,A7,A8,A10,A11,A18,A25,A50,AFF_1:18;
end;
not P // C by A2,A25,AFF_1:44;
then consider s such that
A51: s in P and
A52: s in C by A10,A11,AFF_1:58;
A53: LIN s,c,c9 by A7,A8,A11,A52,AFF_1:21;
A54: b<>b9
proof
assume b=b9;
then b,a // b,a9 by A14,AFF_1:4;
then LIN b,a,a9 by AFF_1:def 1;
then LIN a,a9,b by AFF_1:6;
then b in A by A3,A4,A9,A29,AFF_1:25;
hence contradiction by A2,A5,A12,AFF_1:45;
end;
A55: s<>b
proof
assume
A56: s=b;
b,c // c9,b9 by A16,AFF_1:4;
then b9 in C by A7,A8,A11,A48,A52,A56,AFF_1:48;
hence contradiction by A2,A5,A6,A10,A11,A25,A54,A52,A56,AFF_1:18;
end;
consider M such that
A57: c in M and
A58: A // M by A9,AFF_1:49;
A59: M is being_line by A58,AFF_1:36;
A60: b in P9 by A35,AFF_1:24;
not M // P9
proof
assume M // P9;
then A // P9 by A58,AFF_1:44;
then b in A by A3,A60,A47,AFF_1:45;
hence contradiction by A2,A5,A12,AFF_1:45;
end;
then consider p such that
A61: p in M and
A62: p in P9 by A59,A36,AFF_1:58;
M // P by A2,A58,AFF_1:44;
then
A63: c,p // P by A57,A61,AFF_1:40;
A64: M // N by A58,A38,AFF_1:44;
then
A65: c,p // c9,q by A57,A37,A61,A41,AFF_1:39;
A66: now
assume p=q;
then M=N by A64,A61,A41,AFF_1:45;
hence contradiction by A7,A8,A11,A18,A25,A57,A58,A37,A59,AFF_1:18;
end;
A67: P9 // C9 by A14,A35,A19,AFF_1:37;
then
A68: p,b // q,b9 by A60,A39,A62,A42,AFF_1:39;
A69: q,a9 // p,a by A47,A20,A67,A62,A42,AFF_1:39;
c9,q // c,p by A57,A37,A64,A61,A41,AFF_1:39;
then LIN o,q,p by A1,A3,A4,A9,A26,A28,A22,A45,A69,A43,A44,A33;
then
A70: LIN p,q,o by AFF_1:6;
c <>p by A17,A36,A60,A47,A62,AFF_1:21;
then LIN s,p,q by A1,A5,A6,A10,A51,A53,A63,A68,A49,A55,A65,A46;
then
A71: LIN p,q,s by AFF_1:6;
LIN p,q,p by AFF_1:7;
then o=s or p in C by A11,A27,A52,A70,A71,A66,AFF_1:8,25;
then c in P9 by A2,A7,A11,A12,A25,A26,A57,A58,A59,A61,A62,A51,AFF_1:18,45;
hence contradiction by A17,A36,A60,A47,AFF_1:21;
end;
theorem
AP is Moufangian implies AP is translational
proof
assume AP is Moufangian;
then AP is satisfying_des_1 by Th3,Th13;
hence thesis by Th7;
end;
theorem
AP is translational implies AP is satisfying_pap
proof
assume
A1: AP is translational;
let M,N,a,b,c,a9,b9,c9;
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M<>N and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9;
set A=Line(a,b9), A9=Line(b,a9), P=Line(b,c9), P9=Line(c,b9);
A14: c <>b9 by A6,A7,A8,A10,AFF_1:45;
then
A15: c in P9 & b9 in P9 by AFF_1:24;
A16: b<>c9 by A5,A7,A8,A11,AFF_1:45;
then
A17: P is being_line & b in P by AFF_1:24;
A18: P9 is being_line by A14,AFF_1:24;
then consider C9 such that
A19: a in C9 and
A20: P9 // C9 by AFF_1:49;
A21: C9 is being_line by A20,AFF_1:36;
assume
A22: not thesis;
A23: now
assume
A24: a=c;
then b,c9 // b,a9 by A12,A13,A14,AFF_1:5;
then LIN b,c9,a9 by AFF_1:def 1;
then LIN a9,c9,b by AFF_1:6;
then a9=c9 or b in N by A3,A9,A11,AFF_1:25;
hence contradiction by A5,A7,A8,A22,A24,AFF_1:2,45;
end;
A25: P9<>C9
proof
assume P9=C9;
then LIN a,c,b9 by A18,A15,A19,AFF_1:21;
then b9 in M by A2,A4,A6,A23,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
A26: c9 in P by A16,AFF_1:24;
then
A27: P9 // P by A13,A16,A14,A18,A17,A15,AFF_1:38;
A28: now
assume
A29: b=c;
then LIN b,c9,b9 by A13,AFF_1:def 1;
then LIN b9,c9,b by AFF_1:6;
then b9=c9 or b in N by A3,A10,A11,AFF_1:25;
hence contradiction by A5,A7,A8,A12,A22,A29,AFF_1:45;
end;
A30: P9<>P
proof
assume P9=P;
then LIN b,c,b9 by A17,A15,AFF_1:21;
then b9 in M by A2,A5,A6,A28,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
A31: a<>b9 by A4,A7,A8,A10,AFF_1:45;
then
A32: A is being_line by AFF_1:24;
then consider C such that
A33: c in C and
A34: A // C by AFF_1:49;
A35: C is being_line by A34,AFF_1:36;
A36: a,b // b9,a9 by A4,A5,A7,A9,A10,AFF_1:39;
A37: b9,c9 // c,b by A5,A6,A7,A10,A11,AFF_1:39;
A38: b<>a9 by A5,A7,A8,A9,AFF_1:45;
then
A39: a9 in A9 by AFF_1:24;
A40: a in A & b9 in A by A31,AFF_1:24;
A41: A<>C
proof
assume A=C;
then LIN a,c,b9 by A32,A40,A33,AFF_1:21;
then b9 in M by A2,A4,A6,A23,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
not C // C9
proof
assume C // C9;
then A // C9 by A34,AFF_1:44;
then A // P9 by A20,AFF_1:44;
then b9,a // b9,c by A40,A15,AFF_1:39;
then LIN b9,a,c by AFF_1:def 1;
then LIN a,c,b9 by AFF_1:6;
then b9 in M by A2,A4,A6,A23,AFF_1:25;
hence contradiction by A7,A8,A10,AFF_1:45;
end;
then consider s such that
A42: s in C and
A43: s in C9 by A35,A21,AFF_1:58;
A44: A9 is being_line & b in A9 by A38,AFF_1:24;
A45: now
assume
A46: a=b;
then LIN a,b9,a9 by A12,AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then a9=b9 or a in N by A3,A9,A10,AFF_1:25;
hence contradiction by A4,A7,A8,A13,A22,A46,AFF_1:45;
end;
A47: now
assume a9=b9;
then a9,a // a9,b by A12,AFF_1:4;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:6;
then a9 in M by A2,A4,A5,A45,AFF_1:25;
hence contradiction by A7,A8,A9,AFF_1:45;
end;
A48: A<>A9
proof
assume A=A9;
then LIN a9,b9,a by A32,A40,A39,AFF_1:21;
then a in N by A3,A9,A10,A47,AFF_1:25;
hence contradiction by A4,A7,A8,AFF_1:45;
end;
A49: b<>s
proof
assume b=s;
then a,b9 // b,c by A40,A33,A34,A42,AFF_1:39;
then b,a9 // b,c by A12,A31,AFF_1:5;
then LIN b,a9,c by AFF_1:def 1;
then LIN b,c,a9 by AFF_1:6;
then a9 in M by A2,A5,A6,A28,AFF_1:25;
hence contradiction by A7,A8,A9,AFF_1:45;
end;
A50: A // A9 by A12,A31,A38,AFF_1:37;
a,s // b9,c by A15,A19,A20,A43,AFF_1:39;
then
A51: b,s // a9,c by A1,A32,A40,A44,A39,A33,A34,A35,A42,A36,A48,A41,A50;
b9,a // c,s by A40,A33,A34,A42,AFF_1:39;
then c9,a // b,s by A1,A18,A17,A26,A15,A19,A20,A21,A43,A37,A30,A25,A27;
then c9,a // a9,c by A51,A49,AFF_1:5;
hence contradiction by A22,AFF_1:4;
end;