:: Homotheties and Shears in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received September 21, 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, FUNCT_2, STRUCT_0, AFF_2, ANALOAF, INCSP_1,
AFF_1, TRANSGEO, FUNCT_1, RELAT_1, TARSKI, HOMOTHET;
notations TARSKI, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF,
AFF_1, AFF_2, TRANSGEO;
constructors PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
registrations STRUCT_0;
requirements SUBSET, BOOLE;
theorems TRANSGEO, AFF_1, AFF_2, TRANSLAC, SUBSET_1, DIRAF, FUNCT_1, XBOOLE_0;
schemes TRANSGEO;
begin
reserve AFP for AffinPlane;
reserve a,a9,b,b9,c,c9,d,d9,o,p,p9,q,q9,r,s,t,x,y,z for Element of AFP;
reserve A,A9,C,D,P,B9,M,N,K for Subset of AFP;
reserve f for Permutation of the carrier of AFP;
Lm1: AFP is Desarguesian iff for o,a,a9,p,p9,q,q9 st LIN o,a,a9 & LIN o,p,p9 &
LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9
proof
thus AFP is Desarguesian implies for o,a,a9,p,p9,q,q9 st LIN o,a,a9 & LIN o,
p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9
holds p,q // p9,q9
proof
assume
A1: AFP is Desarguesian;
let o,a,a9,p,p9,q,q9;
assume that
A2: LIN o,a,a9 and
A3: LIN o,p,p9 and
A4: LIN o,q,q9 and
A5: not LIN o,a,p and
A6: not LIN o,a,q and
A7: a,p // a9,p9 and
A8: a,q // a9,q9;
set A=Line(o,a), P=Line(o,p), C=Line(o,q);
A9: a in A by AFF_1:15;
A10: o<>a by A5,AFF_1:7;
then
A11: A is being_line by AFF_1:def 3;
A12: o in A by AFF_1:15;
then
A13: a9 in A by A2,A10,A11,A9,AFF_1:25;
A14: q in C by AFF_1:15;
then
A15: A<>C by A6,A11,A12,A9,AFF_1:21;
A16: o in P by AFF_1:15;
A17: p in P by AFF_1:15;
A18: o<>p by A5,AFF_1:7;
then
A19: P is being_line by AFF_1:def 3;
then
A20: p9 in P by A3,A18,A16,A17,AFF_1:25;
A21: o in C by AFF_1:15;
A22: o<>q by A6,AFF_1:7;
then
A23: C is being_line by AFF_1:def 3;
then
A24: q9 in C by A4,A22,A21,A14,AFF_1:25;
A<>P by A5,A11,A12,A9,A17,AFF_1:21;
hence thesis by A1,A7,A8,A10,A18,A22,A11,A19,A23,A12,A9,A16,A17,A21,A14,A13
,A20,A24,A15,AFF_2:def 4;
end;
assume
A25: for o,a,a9,p,p9,q,q9 st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not
LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9;
now
let A,P,C,o,a,b,c,a9,b9,c9;
assume that
A26: o in A and
A27: o in P and
A28: o in C and
A29: o<>a and
A30: o<>b and
A31: o<>c and
A32: a in A and
A33: a9 in A and
A34: b in P and
A35: b9 in P and
A36: c in C and
A37: c9 in C and
A38: A is being_line and
A39: P is being_line and
A40: C is being_line and
A41: A<>P and
A42: A<>C and
A43: a,b // a9,b9 and
A44: a,c // a9,c9;
A45: LIN o,b,b9 by A27,A34,A35,A39,AFF_1:21;
A46: not LIN o,a,c
proof
assume LIN o,a,c;
then c in A by A26,A29,A32,A38,AFF_1:25;
hence contradiction by A26,A28,A31,A36,A38,A40,A42,AFF_1:18;
end;
A47: not LIN o,a,b
proof
assume LIN o,a,b;
then b in A by A26,A29,A32,A38,AFF_1:25;
hence contradiction by A26,A27,A30,A34,A38,A39,A41,AFF_1:18;
end;
A48: LIN o,c,c9 by A28,A36,A37,A40,AFF_1:21;
LIN o,a,a9 by A26,A32,A33,A38,AFF_1:21;
hence b,c // b9,c9 by A25,A43,A44,A45,A48,A47,A46;
end;
hence thesis by AFF_2:def 4;
end;
Lm2: AFP is Moufangian iff for o,K,c,c9,a,b,a9,b9 st o in K & c in K & c9 in K
& K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 //
K & a,c // a9,c9 holds b,c // b9,c9
proof
thus AFP is Moufangian implies for o,K,c,c9,a,b,a9,b9 st o in K & c in K &
c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K &
a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9
proof
assume
A1: AFP is Moufangian;
let o,K,c,c9,a,b,a9,b9;
assume that
A2: o in K and
A3: c in K and
A4: c9 in K and
A5: K is being_line and
A6: LIN o,a,a9 and
A7: LIN o,b,b9 and
A8: not a in K and
A9: a,b // K and
A10: a9,b9 // K and
A11: a,c // a9,c9;
A12: a,b // a9,b9 by A5,A9,A10,AFF_1:31;
A13: now
A14: now
assume
A15: a=b;
A16: now
A17: not o,a // K by A2,A8,AFF_1:34,35;
A18: LIN o,b9,b by A7,AFF_1:6;
assume that
A19: a9,o // K and
A20: a9<>b9;
o,a // o,a9 by A6,AFF_1:def 1;
then a9,o // o,a by AFF_1:4;
then
A21: o,a // K or a9=o by A19,AFF_1:32;
then b9 in K by A2,A5,A8,A10,AFF_1:23;
hence contradiction by A2,A5,A8,A15,A20,A21,A17,A18,AFF_1:25;
end;
LIN o,a,o by AFF_1:7;
then LIN a9,b9,o by A2,A6,A7,A8,A15,AFF_1:8;
then a9,b9 // a9,o by AFF_1:def 1;
hence thesis by A10,A11,A15,A16,AFF_1:32;
end;
assume o<>c;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A11,A12,A14,AFF_2:def 7;
end;
now
assume
A22: o=c;
then LIN b,b9,c by A7,AFF_1:6;
then
A23: b,b9 // b,c by AFF_1:def 1;
LIN a,c,a9 by A6,A22,AFF_1:6;
then LIN a,c,c9 by A3,A8,A11,AFF_1:9;
then
A24: LIN c,c9,a by AFF_1:6;
then LIN c9,b,b9 by A2,A4,A5,A7,A8,A22,AFF_1:25;
then LIN b9,b,c9 by AFF_1:6;
then b9,b // b9,c9 by AFF_1:def 1;
then
A25: b,b9 // b9,c9 by AFF_1:4;
c = c9 by A3,A4,A5,A8,A24,AFF_1:25;
then b=b9 implies thesis by AFF_1:2;
hence thesis by A23,A25,AFF_1:5;
end;
hence thesis by A13;
end;
assume
A26: for o,K,c,c9,a,b,a9,b9 st o in K & c in K & c9 in K & K is
being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c
// a9,c9 holds b,c // b9,c9;
now
let K,o,a,b,c,a9,b9,c9;
assume that
A27: K is being_line and
A28: o in K and
A29: c in K and
A30: c9 in K and
A31: not a in K and
o<>c and
A32: a<>b and
A33: LIN o,a,a9 and
A34: LIN o,b,b9 and
A35: a,b // a9,b9 and
A36: a,c // a9,c9 and
A37: a,b // K;
a9,b9 // K by A32,A35,A37,AFF_1:32;
hence b,c // b9,c9 by A26,A27,A28,A29,A30,A31,A33,A34,A36,A37;
end;
hence thesis by AFF_2:def 7;
end;
Lm3: AFP is Moufangian implies 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 & 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
proof
assume
A1: AFP is Moufangian;
thus 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 & 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
proof
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: a<>b and
A8: LIN o,a,a9 and
A9: a,b // a9,b9 and
A10: b,c // b9,c9 and
A11: a,c // a9,c9 and
A12: a,b // K;
consider P such that
A13: a9 in P and
A14: K // P by A2,AFF_1:49;
A15: P is being_line by A14,AFF_1:36;
set A=Line(o,b), C=Line(o,a);
A16: o in A by AFF_1:15;
A17: 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,A12,AFF_1:35;
not A // P
proof
assume A // P;
then A // K by A14,AFF_1:44;
hence contradiction by A3,A20,A16,A17,AFF_1:45;
end;
then consider x such that
A21: x in A and
A22: x in P by A19,A15,AFF_1:58;
A23: o in C by AFF_1:15;
a,b // P by A12,A14,AFF_1:43;
then a9,b9 // P by A7,A9,AFF_1:32;
then
A24: b9 in P by A13,A15,AFF_1:23;
then
A25: LIN b9,x,b9 by A15,A22,AFF_1:21;
A26: a in C by AFF_1:15;
A27: LIN o,b,x by A19,A16,A17,A21,AFF_1:21;
A28: C is being_line by A3,A6,AFF_1:def 3;
then
A29: a9 in C by A3,A6,A8,A23,A26,AFF_1:25;
A30: b9<>c9
proof
A31: a9,c9 // c,a by A11,AFF_1:4;
assume
A32: b9=c9;
then P=K by A5,A14,A24,AFF_1:45;
then a9=o by A2,A3,A6,A28,A23,A26,A29,A13,AFF_1:18;
then b9=o by A2,A3,A4,A5,A6,A32,A31,AFF_1:48;
hence contradiction by A18,AFF_1:7;
end;
A33: a9<>b9
proof
assume
A34: a9=b9;
A35: now
assume a9=c9;
then b9=o by A2,A3,A5,A6,A28,A23,A26,A29,A34,AFF_1:18;
hence contradiction by A18,AFF_1:7;
end;
a,c // b,c or a9=c9 by A10,A11,A34,AFF_1:5;
then c,a // c,b by A35,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 A7,A12,AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2,A4,A6,AFF_1:23;
end;
A36: b<>c by A4,A6,A12,AFF_1:35;
a9,x // K by A13,A14,A22,AFF_1:40;
then b,c // x,c9 by A1,A2,A3,A4,A5,A6,A8,A11,A12,A27,Lm2;
then b9,c9 // x,c9 by A10,A36,AFF_1:5;
then c9,b9 // c9,x by AFF_1:4;
then LIN c9,b9,x by AFF_1:def 1;
then
A37: LIN b9,x,c9 by AFF_1:6;
LIN b9,x,a9 by A13,A15,A22,A24,AFF_1:21;
then LIN b9,c9,a9 by A18,A27,A37,A25,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 A10,A30,AFF_1:5;
then a,b // b,c by A9,A33,AFF_1:5;
then b,c // K by A7,A12,AFF_1:32;
then c,b // K by AFF_1:34;
hence contradiction by A2,A4,A20,AFF_1:23;
end;
end;
Lm4: AFP is Moufangian implies for K,A,C,p,q,a,a9,b,b9 st K // A & K // C & K
<>A & K<>C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,
a9 & p,b // q,b9 holds a,b // a9,b9
proof
assume AFP is Moufangian;
then
A1: AFP is translational by AFF_2:14;
let K,A,C,p,q,a,a9,b,b9;
assume that
A2: K // A and
A3: K // C and
A4: K<>A and
A5: K<>C and
A6: p in K and
A7: q in K and
A8: a in A and
A9: a9 in A and
A10: b in C and
A11: b9 in C and
A12: p,a // q,a9 and
A13: p,b // q,b9;
A14: A is being_line by A2,AFF_1:36;
A15: C is being_line by A3,AFF_1:36;
K is being_line by A2,AFF_1:36;
hence thesis by A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A1,A14,A15,
AFF_2:def 11;
end;
theorem Th1:
not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 &
LIN o,p,q & LIN o,p,q9 & p<>q & o<>q & o<>x & a,p // b,p9 & a,q // b,q9 & x,p
// y,p9 & AFP is Desarguesian implies x,q // y,q9
proof
assume that
A1: not LIN o,a,p and
A2: LIN o,a,b and
A3: LIN o,a,x and
A4: LIN o,a,y and
A5: LIN o,p,p9 and
A6: LIN o,p,q and
A7: LIN o,p,q9 and
A8: p<>q and
A9: o<>q and
A10: o<>x and
A11: a,p // b,p9 and
A12: a,q // b,q9 and
A13: x,p // y,p9 and
A14: AFP is Desarguesian;
set B9=Line(o,p);
A15: o in B9 by AFF_1:15;
A16: o<>p by A1,AFF_1:7;
then consider d such that
A17: LIN x,p,d and
A18: d<>x and
A19: d<>p by A6,A8,A9,TRANSLAC:1;
A20: B9 is being_line by A16,AFF_1:def 3;
A21: q9 in B9 by A7,AFF_1:def 2;
q in B9 by A6,AFF_1:def 2;
then
A22: LIN o,q,q9 by A20,A15,A21,AFF_1:21;
set A=Line(o,a);
o<>a by A1,AFF_1:7;
then
A23: A is being_line by AFF_1:def 3;
A24: y in A by A4,AFF_1:def 2;
A25: p,a // p9,b by A11,AFF_1:4;
A26: not LIN o,p,a by A1,AFF_1:6;
set K=Line(x,p);
A27: K is being_line by A1,A3,AFF_1:def 3;
then consider M such that
A28: y in M and
A29: K // M by AFF_1:49;
A30: x in K by AFF_1:15;
A31: M is being_line by A29,AFF_1:36;
A32: p in K by AFF_1:15;
A33: d in K by A17,AFF_1:def 2;
A34: x in A by A3,AFF_1:def 2;
A35: not LIN o,a,d
proof
assume LIN o,a,d;
then d in A by AFF_1:def 2;
then A=K by A18,A27,A30,A33,A23,A34,AFF_1:18;
hence contradiction by A1,A32,AFF_1:def 2;
end;
A36: o in A by AFF_1:15;
not o,d // M
proof
assume o,d // M;
then o,d // K by A29,AFF_1:43;
then d,o // K by AFF_1:34;
then o in K by A27,A33,AFF_1:23;
then A=K by A10,A27,A30,A23,A36,A34,AFF_1:18;
hence contradiction by A1,A32,AFF_1:def 2;
end;
then consider d9 such that
A37: d9 in M and
A38: LIN o,d,d9 by A31,AFF_1:59;
A39: d,x // d9,y by A30,A33,A28,A29,A37,AFF_1:39;
A40: p in B9 by AFF_1:15;
A41: not LIN o,d,q
proof
assume LIN o,d,q;
then
A42: LIN o,q,d by AFF_1:6;
A43: LIN o,q,o by AFF_1:7;
LIN o,q,p by A6,AFF_1:6;
then LIN o,p,d by A9,A43,A42,AFF_1:8;
then d in B9 by AFF_1:def 2;
then B9=K by A19,A27,A32,A33,A20,A40,AFF_1:18;
then A=B9 by A10,A27,A30,A23,A36,A34,A15,AFF_1:18;
hence contradiction by A1,A40,AFF_1:def 2;
end;
A44: not LIN o,d,x
proof
assume LIN o,d,x;
then LIN o,x,d by AFF_1:6;
then d in A by A10,A23,A36,A34,AFF_1:25;
then A=K by A18,A27,A30,A33,A23,A34,AFF_1:18;
hence contradiction by A1,A32,AFF_1:def 2;
end;
A45: not LIN o,p,d
proof
assume LIN o,p,d;
then d in B9 by AFF_1:def 2;
then K=B9 by A19,A27,A32,A33,A20,A40,AFF_1:18;
hence contradiction by A27,A30,A33,A15,A44,AFF_1:21;
end;
A46: q in B9 by A6,AFF_1:def 2;
A47: not LIN o,a,q
proof
assume LIN o,a,q;
then q in A by AFF_1:def 2;
then A=B9 by A9,A23,A36,A20,A15,A46,AFF_1:18;
hence contradiction by A1,A40,AFF_1:def 2;
end;
x in A by A3,AFF_1:def 2;
then
A48: LIN o,x,y by A23,A36,A24,AFF_1:21;
x,p // K by A27,A30,A32,AFF_1:23;
then x,p // M by A29,AFF_1:43;
then y,p9 // M by A1,A3,A13,AFF_1:32;
then p9 in M by A28,A31,AFF_1:23;
then p,d // p9,d9 by A32,A33,A29,A37,AFF_1:39;
then a,d // b,d9 by A2,A5,A14,A38,A45,A26,A25,Lm1;
then d,q // d9,q9 by A2,A12,A14,A38,A47,A35,A22,Lm1;
hence thesis by A14,A38,A39,A41,A44,A22,A48,Lm1;
end;
theorem Th2:
(for o,a,b st o<>a & o<>b & LIN o,a,b ex f st f is dilatation & f
.o=o & f.a=b) implies AFP is Desarguesian
proof
assume
A1: for o,a,b st o<>a & o<>b & LIN o,a,b ex f st f is dilatation & f.o=o
& f.a=b;
now
let o,a,a9,p,p9,q,q9;
assume that
A2: LIN o,a,a9 and
A3: LIN o,p,p9 and
A4: LIN o,q,q9 and
A5: not LIN o,a,p and
A6: not LIN o,a,q and
A7: a,p // a9,p9 and
A8: a,q // a9,q9;
A9: now
assume
A10: o<>a9;
o<>a by A5,AFF_1:7;
then consider f such that
A11: f is dilatation and
A12: f.o=o and
A13: f.a=a9 by A1,A2,A10;
set s=f.q;
o,q // o,s by A11,A12,TRANSGEO:68;
then
A14: LIN o,q,s by AFF_1:def 1;
set r=f.p;
o,p // o,r by A11,A12,TRANSGEO:68;
then
A15: LIN o,p,r by AFF_1:def 1;
a,q // a9,s by A11,A13,TRANSGEO:68;
then
A16: s=q9 by A2,A4,A6,A8,A14,AFF_1:56;
a,p // a9,r by A11,A13,TRANSGEO:68;
then r=p9 by A2,A3,A5,A7,A15,AFF_1:56;
hence p,q // p9,q9 by A11,A16,TRANSGEO:68;
end;
now
assume
A17: o=a9;
then o=p9 by A3,A5,A7,AFF_1:55;
then p9=q9 by A4,A6,A8,A17,AFF_1:55;
hence p,q // p9,q9 by AFF_1:3;
end;
hence p,q // p9,q9 by A9;
end;
hence thesis by Lm1;
end;
Lm5: o<>a & o<>b & LIN o,a,b & LIN o,a,y & ( not LIN o,a,x & LIN o,x,y & a,x
// b,y or (LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,
x // p9,y & LIN o,a,y)) implies LIN o,a,x
proof
assume that
A1: o<>a and
A2: o<>b and
A3: LIN o,a,b and
A4: LIN o,a,y and
A5: not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y);
assume
A6: not LIN o,a,x;
then
A7: b<>y by A2,A3,A5,AFF_1:54;
set A=Line(o,a);
A8: A is being_line by A1,AFF_1:def 3;
A9: b,y // a,x by A5,A6,AFF_1:4;
A10: a in A by AFF_1:15;
A11: y in A by A4,AFF_1:def 2;
A12: o in A by AFF_1:15;
b in A by A3,AFF_1:def 2;
then A=Line(b,y) by A8,A7,A11,AFF_1:24;
then x in A by A7,A10,A9,AFF_1:22;
hence contradiction by A6,A8,A12,A10,AFF_1:21;
end;
Lm6: o<>a & o<>b & LIN o,a,b & ( not LIN o,a,x & LIN o,x,y & a,x // b,y or (
LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y &
LIN o,a,y)) implies o<>b & o<>a & LIN o,b,a & ( not LIN o,b,y & LIN o,y,x & b,y
// a,x or (LIN o,b,y & ex p,p9 st not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,
y // p9,x & LIN o,b,x))
proof
assume that
A1: o<>a and
A2: o<>b and
A3: LIN o,a,b and
A4: not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y);
A5: LIN o,b,a by A3,AFF_1:6;
A6: now
assume
A7: LIN o,a,x;
then consider p,q such that
A8: not LIN o,a,p and
A9: LIN o,p,q and
A10: a,p // b,q and
A11: p,x // q,y and
A12: LIN o,a,y by A4;
A13: not LIN o,p,a by A8,AFF_1:6;
A14: q,y // p,x by A11,AFF_1:4;
A15: b,q // a,p by A10,AFF_1:4;
A16: LIN o,q,p by A9,AFF_1:6;
LIN o,a,o by AFF_1:7;
then
A17: LIN o,b,x by A1,A3,A7,AFF_1:8;
set A=Line(o,b);
A18: o in A by AFF_1:15;
A19: a in A by A5,AFF_1:def 2;
A20: A is being_line by A2,AFF_1:def 3;
p,a // q,b by A10,AFF_1:4;
then
A21: q<>o by A2,A3,A13,AFF_1:55;
A22: not LIN o,b,q
proof
assume LIN o,b,q;
then q in A by AFF_1:def 2;
then p in A by A21,A20,A18,A16,AFF_1:25;
hence contradiction by A8,A20,A18,A19,AFF_1:21;
end;
y in A by A1,A12,A20,A18,A19,AFF_1:25;
hence thesis by A1,A2,A3,A15,A14,A16,A22,A17,AFF_1:6,def 2;
end;
now
assume
A23: not LIN o,a,x;
then
A24: not LIN o,a,y by A1,A2,A3,A4,Lm5;
not LIN o,b,y
proof
A25: LIN o,b,o by AFF_1:7;
assume
A26: LIN o,b,y;
LIN o,b,a by A3,AFF_1:6;
hence contradiction by A2,A24,A26,A25,AFF_1:8;
end;
hence thesis by A1,A2,A3,A4,A23,AFF_1:4,6;
end;
hence thesis by A6;
end;
Lm7: o<>a & x=o & ( not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex
p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y))
implies y=o
proof
assume that
A1: o<>a and
A2: x=o and
A3: not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y);
consider p,p9 such that
A4: not LIN o,a,p and
A5: LIN o,p,p9 and
a,p // b,p9 and
A6: p,x // p9,y and
A7: LIN o,a,y by A2,A3,AFF_1:7;
set K=Line(o,p);
A8: o<>p by A4,AFF_1:7;
p9 in K by A5,AFF_1:def 2;
then
A9: y in K by A2,A6,A8,AFF_1:22;
assume
A10: y<>o;
A11: o in K by AFF_1:15;
A12: p in K by AFF_1:15;
set A=Line(o,a);
A13: A is being_line by A1,AFF_1:def 3;
A14: a in A by AFF_1:15;
A15: y in A by A7,AFF_1:def 2;
A16: o in A by AFF_1:15;
K is being_line by A8,AFF_1:def 3;
then p in A by A10,A13,A16,A12,A9,A11,A15,AFF_1:18;
hence contradiction by A4,A13,A16,A14,AFF_1:21;
end;
Lm8: for o,a,b,x st o<>a & LIN o,a,b ex y st not LIN o,a,x & LIN o,x,y & a,x
// b,y or (LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,
x // p9,y & LIN o,a,y)
proof
let o,a,b,x such that
A1: o<>a and
A2: LIN o,a,b;
A3: now
consider p such that
A4: not LIN o,a,p by A1,AFF_1:13;
set K=Line(o,p);
o<>p by A4,AFF_1:7;
then
A5: K is being_line by AFF_1:def 3;
set A=Line(a,p);
a<>p by A4,AFF_1:7;
then A is being_line by AFF_1:def 3;
then consider B9 such that
A6: b in B9 and
A7: A // B9 by AFF_1:49;
A8: B9 is being_line by A7,AFF_1:36;
A9: a in A by AFF_1:15;
A10: p in K by AFF_1:15;
A11: p in A by AFF_1:15;
A12: o in K by AFF_1:15;
not B9 // K
proof
assume B9 // K;
then A // K by A7,AFF_1:44;
then A=K by A10,A11,AFF_1:45;
hence contradiction by A4,A12,A10,A9,A5,AFF_1:21;
end;
then consider p9 such that
A13: p9 in B9 and
A14: p9 in K by A5,A8,AFF_1:58;
A15: a,p // b,p9 by A9,A11,A6,A7,A13,AFF_1:39;
set M=Line(o,a);
A16: o in M by AFF_1:15;
o<>a by A4,AFF_1:7;
then
A17: M is being_line by AFF_1:def 3;
set C=Line(p,x);
assume
A18: LIN o,a,x;
then
A19: C is being_line by A4,AFF_1:def 3;
then consider D such that
A20: p9 in D and
A21: C // D by AFF_1:49;
A22: p in C by AFF_1:15;
A23: LIN o,p,p9 by A12,A10,A5,A14,AFF_1:21;
A24: a in M by AFF_1:15;
A25: x in C by AFF_1:15;
A26: x in M by A18,AFF_1:def 2;
A27: not D // M
proof
assume D // M;
then C // M by A21,AFF_1:44;
then C=M by A26,A25,AFF_1:45;
hence contradiction by A4,A16,A24,A22,A19,AFF_1:21;
end;
D is being_line by A21,AFF_1:36;
then consider y such that
A28: y in D and
A29: y in M by A17,A27,AFF_1:58;
A30: LIN o,a,y by A16,A24,A17,A29,AFF_1:21;
p,x // p9,y by A22,A25,A20,A21,A28,AFF_1:39;
hence thesis by A18,A4,A23,A15,A30;
end;
now
o,a // o,b by A2,AFF_1:def 1;
then a,o // o,b by AFF_1:4;
then consider y such that
A31: x,o // o,y and
A32: x,a // b,y by A1,DIRAF:40;
o,x // o,y by A31,AFF_1:4;
then
A33: LIN o,x,y by AFF_1:def 1;
assume
A34: not LIN o,a,x;
a,x // b,y by A32,AFF_1:4;
hence thesis by A34,A33;
end;
hence thesis by A3;
end;
Lm9: for o,a,b,y st o<>a & o<>b & LIN o,a,b ex x st not LIN o,a,x & LIN o,x,y
& a,x // b,y or (LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,
p9 & p,x // p9,y & LIN o,a,y)
proof
let o,a,b,y;
assume that
A1: o<>a and
A2: o<>b and
A3: LIN o,a,b;
A4: LIN o,b,a by A3,AFF_1:6;
then consider x such that
A5: not LIN o,b,y & LIN o,y,x & b,y // a,x or (LIN o,b,y & ex p,p9 st
not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x) by A2,Lm8
;
not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st not
LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y) by A1,A2,A4,A5
,Lm6;
hence thesis;
end;
Lm10: o<>a & a=b & ( not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex
p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y))
implies x=y
proof
assume that
A1: o<>a and
A2: a=b and
A3: not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y);
A4: now
A5: LIN o,x,x by AFF_1:7;
A6: LIN o,a,a by AFF_1:7;
assume that
A7: LIN o,a,x and
A8: x<>o;
consider p,q such that
A9: not LIN o,a,p and
A10: LIN o,p,q and
A11: a,p // b,q and
A12: p,x // q,y and
A13: LIN o,a,y by A3,A7;
A14: LIN o,p,p by AFF_1:7;
A15: not LIN o,p,x
proof
assume LIN o,p,x;
then
A16: LIN o,x,p by AFF_1:6;
A17: LIN o,x,o by AFF_1:7;
LIN o,x,a by A7,AFF_1:6;
hence contradiction by A8,A9,A17,A16,AFF_1:8;
end;
LIN o,a,o by AFF_1:7;
then
A18: LIN o,x,y by A1,A7,A13,AFF_1:8;
a,p // a,p by AFF_1:2;
then
A19: p,x // p,y by A2,A9,A10,A11,A12,A6,A14,AFF_1:56;
p,x // p,x by AFF_1:2;
hence thesis by A14,A15,A18,A19,A5,AFF_1:56;
end;
now
A20: LIN o,x,x by AFF_1:7;
A21: LIN o,a,a by AFF_1:7;
A22: a,x // a,x by AFF_1:2;
assume not LIN o,a,x;
hence thesis by A2,A3,A22,A21,A20,AFF_1:56;
end;
hence thesis by A1,A3,A4,Lm7;
end;
Lm11: o<>a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & (ex p,p9 st not LIN
o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y) & (ex p,p9 st not
LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r) implies y=r
proof
assume that
A1: o<>a and
A2: LIN o,a,b and
A3: AFP is Desarguesian and
A4: LIN o,a,x and
A5: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y &
LIN o,a,y and
A6: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r &
LIN o,a,r;
consider q,q9 such that
A7: not LIN o,a,q and
A8: LIN o,q,q9 and
A9: a,q // b,q9 and
A10: q,x // q9,r and
A11: LIN o,a,r by A6;
A12: o<>q by A7,AFF_1:7;
consider p,p9 such that
A13: not LIN o,a,p and
A14: LIN o,p,p9 and
A15: a,p // b,p9 and
A16: p,x // p9,y and
A17: LIN o,a,y by A5;
A18: a=x implies thesis
proof
A19: q,a // q9,b by A9,AFF_1:4;
A20: not LIN o,q,a by A7,AFF_1:6;
A21: p,a // p9,b by A15,AFF_1:4;
assume
A22: a=x;
not LIN o,p,a by A13,AFF_1:6;
then b=y by A2,A14,A16,A17,A22,A21,AFF_1:56;
hence thesis by A2,A8,A10,A11,A22,A20,A19,AFF_1:56;
end;
A23: o<>p by A13,AFF_1:7;
A24: a<>b & a<>x & p<>q & o<>x implies thesis
proof
assume that
a<>b and
a<>x and
A25: p<>q and
A26: o<>x;
A27: now
set K=Line(o,p);
set A=Line(o,a);
A28: LIN o,q,o by AFF_1:7;
A29: o in A by AFF_1:15;
A30: p in K by AFF_1:15;
A31: o in K by AFF_1:15;
A32: A is being_line by A1,AFF_1:def 3;
A33: x in A by A4,AFF_1:def 2;
r in A by A11,AFF_1:def 2;
then
A34: LIN o,x,r by A32,A29,A33,AFF_1:21;
A35: x,p // y,p9 by A16,AFF_1:4;
assume
A36: LIN o,p,q;
then LIN o,q,p by AFF_1:6;
then LIN o,p,q9 by A8,A12,A28,AFF_1:8;
then x,q // y,q9 by A2,A3,A4,A13,A14,A15,A17,A9,A12,A25,A26,A36,A35,Th1;
then
A37: q,x // q9,y by AFF_1:4;
A38: K is being_line by A23,AFF_1:def 3;
A39: q in K by A36,AFF_1:def 2;
A40: not LIN o,q,x
proof
assume
A41: LIN o,q,x;
K=Line(o,q) by A12,A38,A31,A39,AFF_1:24;
then x in K by A41,AFF_1:def 2;
then
A42: p in A by A26,A32,A29,A33,A38,A31,A30,AFF_1:18;
A43: a in A by AFF_1:15;
A is being_line by A1,AFF_1:def 3;
hence contradiction by A13,A29,A43,A42,AFF_1:21;
end;
y in A by A17,AFF_1:def 2;
then LIN o,x,y by A32,A29,A33,AFF_1:21;
hence thesis by A8,A10,A37,A40,A34,AFF_1:56;
end;
now
A44: not LIN o,p,x
proof
assume LIN o,p,x;
then
A45: LIN o,x,p by AFF_1:6;
LIN o,a,o by AFF_1:7;
hence contradiction by A4,A13,A26,A45,AFF_1:11;
end;
set K=Line(o,q);
set A=Line(o,a);
assume
A46: not LIN o,p,q;
A47: o in A by AFF_1:15;
A48: q in K by AFF_1:15;
A49: o in K by AFF_1:15;
A50: A is being_line by A1,AFF_1:def 3;
A51: x in A by A4,AFF_1:def 2;
A52: y in A by A17,AFF_1:def 2;
then
A53: LIN o,x,y by A50,A47,A51,AFF_1:21;
A54: K is being_line by A12,AFF_1:def 3;
A55: not LIN o,q,x
proof
assume LIN o,q,x;
then x in K by AFF_1:def 2;
then
A56: q in A by A26,A50,A47,A51,A54,A49,A48,AFF_1:18;
A57: a in A by AFF_1:15;
A is being_line by A1,AFF_1:def 3;
hence contradiction by A7,A47,A57,A56,AFF_1:21;
end;
r in A by A11,AFF_1:def 2;
then
A58: LIN o,x,r by A50,A47,A51,AFF_1:21;
A59: LIN o,x,y by A50,A47,A51,A52,AFF_1:21;
p,q // p9,q9 by A2,A3,A13,A14,A15,A7,A8,A9,Lm1;
then q,x // q9,y by A3,A14,A16,A8,A46,A44,A53,Lm1;
hence thesis by A8,A10,A55,A59,A58,AFF_1:56;
end;
hence thesis by A27;
end;
A60: o<>a by A13,AFF_1:7;
A61: p=q & o<>x implies thesis
proof
assume that
A62: p=q and
A63: o<>x;
A64: not LIN o,p,x
proof
assume LIN o,p,x;
then
A65: LIN o,x,p by AFF_1:6;
A66: LIN o,x,o by AFF_1:7;
LIN o,x,a by A4,AFF_1:6;
hence contradiction by A13,A63,A66,A65,AFF_1:8;
end;
A67: LIN o,a,o by AFF_1:7;
then
A68: LIN o,x,y by A4,A17,A60,AFF_1:8;
A69: LIN o,x,r by A4,A11,A60,A67,AFF_1:8;
p9=q9 by A2,A13,A14,A15,A8,A9,A62,AFF_1:56;
hence thesis by A14,A16,A10,A62,A68,A69,A64,AFF_1:56;
end;
A70: o=x implies thesis
proof
assume
A71: o=x;
then y=o by A1,A4,A5,Lm7;
hence thesis by A1,A4,A6,A71,Lm7;
end;
a=b implies thesis
proof
assume
A72: a=b;
then x=y by A1,A4,A5,Lm10;
hence thesis by A1,A4,A6,A72,Lm10;
end;
hence thesis by A70,A61,A18,A24;
end;
Lm12: o<>a & o<>b & LIN o,a,b & AFP is Desarguesian & ( not LIN o,a,x & LIN o,
x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p //
b,p9 & p,x // p9,y & LIN o,a,y)) & ( not LIN o,a,r & LIN o,r,y & a,r // b,y or
(LIN o,a,r & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y
& LIN o,a,y)) implies x=r
proof
assume that
A1: o<>a and
A2: o<>b and
A3: LIN o,a,b and
A4: AFP is Desarguesian and
A5: not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y) and
A6: not LIN o,a,r & LIN o,r,y & a,r // b,y or (LIN o,a,r & ex p,p9 st
not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y);
A7: not LIN o,b,y & LIN o,y,r & b,y // a,r or (LIN o,b,y & ex p,p9 st not
LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,r & LIN o,b,r) by A1,A2,A3,A6
,Lm6;
A8: LIN o,b,a by A3,AFF_1:6;
not LIN o,b,y & LIN o,y,x & b,y // a,x or (LIN o,b,y & ex p,p9 st not
LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x) by A1,A2,A3,A5
,Lm6;
hence thesis by A2,A4,A8,A7,Lm11,AFF_1:56;
end;
Lm13: for o,a,b st AFP is Desarguesian & o<>a & o<>b & LIN o,a,b ex f st for x
,y holds (f.x=y iff ( not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex
p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y)))
proof
let o,a,b;
defpred P[Element of AFP,Element of AFP] means ((not LIN o,a,$1 & LIN o,$1,
$2 & a,$1 // b,$2) or (LIN o,a,$1 & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p
// b,p9 & p,$1 // p9,$2 & LIN o,a,$2));
assume that
A1: AFP is Desarguesian and
A2: o<>a and
A3: o<>b and
A4: LIN o,a,b;
A5: for y ex x st P[x,y] by A2,A3,A4,Lm9;
A6: for x ex y st P[x,y] by A2,A4,Lm8;
A7: for x,y,s st P[x,y] & P[x,s] holds y=s by A1,A2,A4,Lm11,AFF_1:56;
A8: for x,y,r st P[x,y] & P[r,y] holds x=r by A1,A2,A3,A4,Lm12;
ex f st for x,y holds (f.x=y iff P[x,y]) from TRANSGEO:sch 1(A6,A5, A8,
A7);
hence thesis;
end;
Lm14: AFP is Desarguesian & o<>a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x
// b,y & LIN o,a,z & (ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z
// p9,t & LIN o,a,t) implies x,z // y,t
proof
assume that
A1: AFP is Desarguesian and
A2: o<>a and
A3: LIN o,a,b and
A4: not LIN o,a,x and
A5: LIN o,x,y and
A6: a,x // b,y and
A7: LIN o,a,z and
A8: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t &
LIN o,a,t;
consider p,p9 such that
A9: not LIN o,a,p and
A10: LIN o,p,p9 and
A11: a,p // b,p9 and
A12: p,z // p9,t and
A13: LIN o,a,t by A8;
A14: now
A15: p,a // p9,b by A11,AFF_1:4;
assume
A16: a=z;
not LIN o,p,a by A9,AFF_1:6;
then z,x // t,y by A3,A6,A10,A12,A13,A16,A15,AFF_1:56;
hence thesis by AFF_1:4;
end;
A17: p,x // p9,y by A1,A3,A4,A5,A6,A9,A10,A11,Lm1;
A18: now
assume that
A19: z<>o and
A20: not LIN o,p,x;
A21: not LIN o,p,z
proof
A22: LIN o,p,o by AFF_1:7;
assume
A23: LIN o,p,z;
LIN o,z,a by A7,AFF_1:6;
then LIN o,p,a by A19,A23,A22,AFF_1:11;
hence contradiction by A9,AFF_1:6;
end;
LIN o,a,o by AFF_1:7;
then LIN o,z,t by A2,A7,A13,AFF_1:8;
hence thesis by A1,A5,A10,A12,A17,A20,A21,Lm1;
end;
A24: o<>x by A4,AFF_1:7;
A25: now
assume that
A26: z<>o and
A27: LIN o,p,x and
a<>z;
now
A28: LIN o,x,o by AFF_1:7;
LIN o,x,p by A27,AFF_1:6;
then
A29: LIN o,p,y by A5,A24,A28,AFF_1:8;
assume
A30: x<>p;
z,p // t,p9 by A12,AFF_1:4;
then z,x // t,y by A1,A3,A6,A7,A9,A10,A11,A13,A24,A26,A27,A30,A29,Th1;
hence thesis by AFF_1:4;
end;
hence thesis by A3,A4,A5,A6,A10,A11,A12,AFF_1:56;
end;
now
A31: o,x // o,y by A5,AFF_1:def 1;
assume
A32: z=o;
then t=o by A2,A7,A8,Lm7;
hence thesis by A32,A31,AFF_1:4;
end;
hence thesis by A18,A14,A25;
end;
Lm15: AFP is Desarguesian & o<>a & LIN o,a,b & LIN o,a,x & (ex p,p9 st not LIN
o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y) & not LIN o,a,z &
LIN o,z,t & a,z // b,t implies x,z // y,t
proof
assume that
A1: AFP is Desarguesian and
A2: o<>a and
A3: LIN o,a,b and
A4: LIN o,a,x and
A5: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y &
LIN o,a,y and
A6: not LIN o,a,z and
A7: LIN o,z,t and
A8: a,z // b,t;
z,x // t,y by A1,A2,A3,A4,A5,A6,A7,A8,Lm14;
hence thesis by AFF_1:4;
end;
Lm16: o<>a & LIN o,a,x & (ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9
& p,x // p9,y & LIN o,a,y) & LIN o,a,z & (ex p,p9 st not LIN o,a,p & LIN o,p,p9
& a,p // b,p9 & p,z // p9,t & LIN o,a,t) implies x,z // y,t
proof
assume that
A1: o<>a and
A2: LIN o,a,x and
A3: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y &
LIN o,a,y and
A4: LIN o,a,z and
A5: ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t &
LIN o,a,t;
set A=Line(o,a);
A6: x in A by A2,AFF_1:def 2;
A7: z in A by A4,AFF_1:def 2;
A8: y in A by A3,AFF_1:def 2;
A9: t in A by A5,AFF_1:def 2;
A10: A is being_line by A1,AFF_1:def 3;
now
assume
A11: x<>z;
then A=Line(x,z) by A10,A6,A7,AFF_1:24;
hence thesis by A8,A9,A11,AFF_1:22;
end;
hence thesis by AFF_1:3;
end;
Lm17: o<>a & LIN o,a,b & AFP is Desarguesian & (for x,y holds (f.x=y iff ((not
LIN o,a,x & LIN o,x,y & a,x // b,y) or (LIN o,a,x & ex p,p9 st not LIN o,a,p &
LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y)))) implies f is dilatation
& f.o=o & f.a=b
proof
assume that
A1: o<>a and
A2: LIN o,a,b and
A3: AFP is Desarguesian;
assume
A4: for x,y holds (f.x=y iff ( not LIN o,a,x & LIN o,x,y & a,x // b,y or
(LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y
& LIN o,a,y)));
for x,r holds x,r // f.x,f.r
proof
let x,r;
set y=f.x;
set s=f.r;
A5: not LIN o,a,r & LIN o,r,s & a,r // b,s or (LIN o,a,r & ex p,p9 st not
LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,s & LIN o,a,s) by A4;
not LIN o,a,x & LIN o,x,y & a,x // b,y or (LIN o,a,x & ex p,p9 st not
LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y) by A4;
hence thesis by A1,A2,A3,A5,Lm1,Lm14,Lm15,Lm16;
end;
hence f is dilatation by TRANSGEO:68;
thus f.o=o
proof
set y=f.o;
not LIN o,a,o & LIN o,o,y & a,o // b,y or (LIN o,a,o & ex p,p9 st not
LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,o // p9,y & LIN o,a,y) by A4;
hence thesis by A1,Lm7;
end;
thus f.a=b
proof
set y=f.a;
LIN o,a,a by AFF_1:7;
then consider p,p9 such that
A6: not LIN o,a,p and
A7: LIN o,p,p9 and
A8: a,p // b,p9 and
A9: p,a // p9,y and
A10: LIN o,a,y by A4;
A11: p,a // p9,b by A8,AFF_1:4;
not LIN o,p,a by A6,AFF_1:6;
hence thesis by A2,A7,A9,A10,A11,AFF_1:56;
end;
end;
theorem Th3:
AFP is Desarguesian implies for o,a,b st o<>a & o<>b & LIN o,a,b
ex f st f is dilatation & f.o=o & f.a=b
proof
assume
A1: AFP is Desarguesian;
let o,a,b;
assume that
A2: o<>a and
A3: o<>b and
A4: LIN o,a,b;
consider f such that
A5: for x,y holds (f.x=y iff ( not LIN o,a,x & LIN o,x,y & a,x // b,y or
(LIN o,a,x & ex p,p9 st not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y
& LIN o,a,y))) by A1,A2,A3,A4,Lm13;
A6: f.a=b by A1,A2,A4,A5,Lm17;
A7: f.o=o by A1,A2,A4,A5,Lm17;
f is dilatation by A1,A2,A4,A5,Lm17;
hence thesis by A7,A6;
end;
theorem
AFP is Desarguesian iff for o,a,b st o<>a & o<>b & LIN o,a,b ex f st f
is dilatation & f.o=o & f.a=b by Th2,Th3;
definition
let AFP,f,K;
pred f is_Sc K means
f is collineation & K is being_line & (for x st
x in K holds f.x = x) & for x holds x,f.x // K;
end;
theorem Th5:
f is_Sc K & f.p=p & not p in K implies f=id the carrier of AFP
by TRANSGEO:97;
theorem Th6:
(for a,b,K st a,b // K & not a in K ex f st f is_Sc K & f.a=b)
implies AFP is Moufangian
proof
assume
A1: for a,b,K st a,b // K & not a in K ex f st f is_Sc K & f.a=b;
now
let o,K,c,c9,a,b,a9,b9;
assume that
A2: o in K and
A3: c in K and
A4: c9 in K and
A5: K is being_line and
A6: LIN o,a,a9 and
A7: LIN o,b,b9 and
A8: not a in K and
A9: a,b // K and
A10: a9,b9 // K and
A11: a,c // a9,c9;
consider f such that
A12: f is_Sc K and
A13: f.a=b by A1,A8,A9;
A14: f is collineation by A12;
A15: a,b // a9,b9 by A5,A9,A10,AFF_1:31;
A16: f.a9=b9
proof
set x=f.a9;
A17: now
f.o=o by A2,A12;
then
A18: LIN o,b,x by A6,A13,A14,TRANSGEO:88;
a9,x // K by A12;
then
A19: a,b // a9,x by A5,A9,AFF_1:31;
assume a<>b;
hence thesis by A2,A6,A7,A8,A9,A15,A19,A18,AFF_1:46,56;
end;
now
assume
A20: a=b;
then f=id the carrier of AFP by A8,A12,A13,Th5;
then x=a9 by FUNCT_1:18;
hence thesis by A2,A6,A7,A8,A10,A20,AFF_1:47;
end;
hence thesis by A17;
end;
A21: f.c9=c9 by A4,A12;
f.c = c by A3,A12;
hence b,c // b9,c9 by A11,A13,A14,A21,A16,TRANSGEO:87;
end;
hence thesis by Lm2;
end;
Lm18: a,b // K & not a in K & ( x in K & x=y or (not x in K & ex p,p9 st p in
K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)) implies b,a // K & not b
in K & ( y in K & y=x or (not y in K & ex p,p9 st p in K & p9 in K & p,b // p9,
y & p,a // p9,x & y,x // K)) by AFF_1:34,35;
Lm19: a,b // K & not a in K implies for x ex y st ( x in K & x=y or (not x in
K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))
proof
assume that
A1: a,b // K and
A2: not a in K;
A3: not b in K by A1,A2,AFF_1:35;
A4: K is being_line by A1,AFF_1:26;
let x;
consider p,q such that
A5: p in K and
q in K and
p<>q by A1,AFF_1:19,26;
A6: p<>b by A1,A2,A5,AFF_1:35;
now
set B9=Line(p,b);
set A=Line(p,a);
assume
A7: not x in K;
A8: a in A by AFF_1:15;
A is being_line by A2,A5,AFF_1:def 3;
then consider C such that
A9: x in C and
A10: A // C by AFF_1:49;
A11: C is being_line by A10,AFF_1:36;
A12: p in A by AFF_1:15;
then not A // K by A2,A5,A8,AFF_1:45;
then not C // K by A10,AFF_1:44;
then consider p9 such that
A13: p9 in C and
A14: p9 in K by A4,A11,AFF_1:58;
B9 is being_line by A6,AFF_1:def 3;
then consider D such that
A15: p9 in D and
A16: B9 // D by AFF_1:49;
A17: b in B9 by AFF_1:15;
K is being_line by A1,AFF_1:26; then
consider M such that
A18: x in M and
A19: K // M by AFF_1:49;
A20: M is being_line by A19,AFF_1:36;
A21: p in B9 by AFF_1:15;
then
A22: not B9 // K by A5,A3,A17,AFF_1:45;
A23: not D // M
proof
assume D // M;
then B9 // M by A16,AFF_1:44;
hence contradiction by A22,A19,AFF_1:44;
end;
D is being_line by A16,AFF_1:36;
then consider y such that
A24: y in D and
A25: y in M by A20,A23,AFF_1:58;
A26: p,b // p9,y by A21,A17,A15,A16,A24,AFF_1:39;
A27: x,y // K by A18,A19,A25,AFF_1:40;
p,a // p9,x by A12,A8,A9,A10,A13,AFF_1:39;
hence thesis by A5,A7,A14,A27,A26;
end;
hence thesis;
end;
Lm20: a,b // K & not a in K implies for y ex x st ( x in K & x=y or (not x in
K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))
proof
assume that
A1: a,b // K and
A2: not a in K;
let y;
A3: b,a // K by A1,AFF_1:34;
A4: not b in K by A1,A2,AFF_1:35;
then consider x such that
A5: y in K & y=x or (not y in K & ex p,p9 st p in K & p9 in K & p,b //
p9,y & p,a // p9,x & y,x // K) by A3,Lm19;
x in K & x=y or (not x in K & ex p,p9 st p in K & p9 in K & p,a // p9,x
& p,b // p9,y & x,y // K) by A3,A4,A5,Lm18;
hence thesis;
end;
theorem Th7:
K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian
& a in M & b in M & x in M & y in M & a<>b & q<>p & p,a // p9,x & p,b // p9,y &
q,a // q9,x implies q,b // q9,y
proof
assume that
A1: K // M and
A2: p in K and
A3: q in K and
A4: p9 in K and
A5: q9 in K and
A6: AFP is Moufangian and
A7: a in M and
A8: b in M and
A9: x in M and
A10: y in M and
A11: a<>b and
A12: q<>p and
A13: p,a // p9,x and
A14: p,b // p9,y and
A15: q,a // q9,x;
A16: K is being_line by A1,AFF_1:36;
A17: M is being_line by A1,AFF_1:36;
now
set D9=Line(q9,x);
set B99=Line(p9,y);
set D=Line(q,a);
set B9=Line(p,b);
A18: q in D by AFF_1:15;
A19: a in D by AFF_1:15;
A20: x in D9 by AFF_1:15;
A21: q9 in D9 by AFF_1:15;
A22: LIN p,q,q9 by A2,A3,A5,A16,AFF_1:21;
A23: LIN p,q,p9 by A2,A3,A4,A16,AFF_1:21;
assume
A24: K<>M;
then
A25: q9<>x by A1,A5,A9,AFF_1:45;
A26: not a in K by A1,A7,A24,AFF_1:45;
A27: b<>p by A1,A2,A8,A24,AFF_1:45;
then
A28: B9 is being_line by AFF_1:def 3;
A29: not q in M by A1,A3,A24,AFF_1:45;
A30: not p in M by A1,A2,A24,AFF_1:45;
A31: LIN a,b,x by A7,A8,A9,A17,AFF_1:21;
A32: now
A33: now
assume that
A34: q=p9 and
A35: q=q9;
LIN q,a,x by A15,A35,AFF_1:def 1;
then LIN a,x,q by AFF_1:6;
then a=x by A7,A9,A17,A29,AFF_1:25;
then a,q // a,p by A13,A34,AFF_1:4;
then LIN a,q,p by AFF_1:def 1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2,A3,A12,A16,A26,AFF_1:25;
end;
A36: now
assume that
A37: p=p9 and
A38: p=q9;
LIN p,a,x by A13,A37,AFF_1:def 1;
then LIN a,x,p by AFF_1:6;
then a=x by A7,A9,A17,A30,AFF_1:25;
then a,q // a,q9 by A15,AFF_1:4;
then LIN a,q,q9 by AFF_1:def 1;
then LIN p,q,a by A38,AFF_1:6;
hence contradiction by A2,A3,A12,A16,A26,AFF_1:25;
end;
assume
A39: not ex a,b,c st LIN a,b,c & a<>b & a<>c & b<>c;
A40: now
assume that
A41: q=p9 and
A42: p=q9;
A43: now
assume
A44: b=x;
then q,y // q,a by A14,A15,A27,A41,A42,AFF_1:5;
then LIN q,y,a by AFF_1:def 1;
then LIN a,y,q by AFF_1:6;
then q9,y // q,b by A7,A10,A13,A17,A29,A41,A42,A44,AFF_1:25;
hence thesis by AFF_1:4;
end;
now
assume a=x;
then a,p // a,q by A13,A41,AFF_1:4;
then LIN a,p,q by AFF_1:def 1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2,A3,A12,A16,A26,AFF_1:25;
end;
hence thesis by A11,A31,A39,A43;
end;
now
assume that
A45: p=p9 and
A46: q=q9;
LIN p,b,y by A14,A45,AFF_1:def 1;
then LIN b,y,p by AFF_1:6;
then b=y by A8,A10,A17,A30,AFF_1:25;
hence thesis by A46,AFF_1:2;
end;
hence thesis by A12,A23,A22,A39,A36,A33,A40;
end;
A47: y in B99 by AFF_1:15;
A48: p9 in B99 by AFF_1:15;
A49: b in B9 by AFF_1:15;
then
A50: B9<>K by A1,A8,A24,AFF_1:45;
a<>q by A1,A3,A7,A24,AFF_1:45;
then
A51: D // D9 by A15,A25,AFF_1:37;
A52: p in B9 by AFF_1:15;
then
A53: B9<>M by A1,A2,A24,AFF_1:45;
A54: p9<>y by A1,A4,A10,A24,AFF_1:45;
then
A55: B9 // B99 by A14,A27,AFF_1:37;
A56: B99 is being_line by A54,AFF_1:def 3;
now
A57: a,q // x,q9 by A18,A19,A21,A20,A51,AFF_1:39;
assume ex a,b,c st LIN a,b,c & a<>b & a<>c & b<>c;
then consider d such that
A58: LIN p,b,d and
A59: d<>p and
A60: d<>b by TRANSLAC:1;
consider N such that
A61: d in N and
A62: K // N by A16,AFF_1:49;
A63: d in B9 by A58,AFF_1:def 2;
then
A64: N<>M by A8,A17,A28,A49,A53,A60,A61,AFF_1:18;
A65: not B99 // N
proof
assume B99 // N;
then B9 // N by A55,AFF_1:44;
then B9 // K by A62,AFF_1:44;
hence contradiction by A2,A52,A50,AFF_1:45;
end;
N is being_line by A62,AFF_1:36;
then consider z such that
A66: z in B99 and
A67: z in N by A56,A65,AFF_1:58;
A68: d,b // z,y by A49,A47,A55,A63,A66,AFF_1:39;
A69: N<>K by A2,A16,A28,A52,A50,A59,A63,A61,AFF_1:18;
A70: M // N by A1,A62,AFF_1:44;
A71: K<>N by A2,A16,A28,A52,A50,A59,A63,A61,AFF_1:18;
A72: N // M by A1,A62,AFF_1:44;
p,d // p9,z by A52,A48,A55,A63,A66,AFF_1:39;
then
A73: a,d // x,z by A1,A2,A4,A6,A7,A9,A13,A24,A61,A62,A67,A71,Lm4;
M<>N by A8,A17,A28,A49,A53,A60,A63,A61,AFF_1:18;
then d,q // z,q9 by A1,A3,A5,A6,A7,A9,A24,A61,A67,A73,A57,A70,Lm4;
hence thesis by A3,A5,A6,A8,A10,A61,A62,A67,A68,A72,A64,A69,Lm4;
end;
hence thesis by A32;
end;
hence thesis by A1,A3,A5,A8,A10,AFF_1:39;
end;
Lm21: a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in
K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x
implies q,b // q9,y
proof
assume that
A1: a,b // K and
A2: not a in K and
A3: not x in K and
A4: AFP is Moufangian and
A5: p in K and
A6: p9 in K and
A7: p,a // p9,x and
A8: p,b // p9,y and
A9: x,y // K and
A10: q in K and
A11: q9 in K and
A12: q,a // q9,x;
A13: K is being_line by A1,AFF_1:26;
A14: now
A15: a,q // x,q9 by A12,AFF_1:4;
A16: b,p // y,p9 by A8,AFF_1:4;
A17: a,p // x,p9 by A7,AFF_1:4;
set A=Line(a,x);
assume that
A18: not a,x // K and
A19: a<>b;
a<>x by A13,A18,AFF_1:33;
then
A20: A is being_line by AFF_1:def 3;
A21: x in A by AFF_1:15;
A22: a in A by AFF_1:15;
then consider o such that
A23: o in A and
A24: o in K by A13,A18,A21,A20,AFF_1:40,58;
A25: LIN o,a,x by A22,A21,A20,A23,AFF_1:21;
K is being_line by A1,AFF_1:26; then
a,b // x,y by A1,A9,AFF_1:31;
then LIN o,b,y by A1,A2,A4,A5,A6,A19,A24,A25,A17,A16,Lm3,AFF_1:26;
then b,q // y,q9 by A1,A2,A4,A9,A10,A11,A13,A24,A25,A15,Lm2;
hence thesis by AFF_1:4;
end;
A26: now
set M=Line(a,b);
assume that
A27: a,x // K and
A28: a<>b and
A29: p<>q;
A30: M is being_line by A28,AFF_1:def 3;
K is being_line by A1,AFF_1:26; then
a,b // a,x by A1,A27,AFF_1:31;
then LIN a,b,x by AFF_1:def 1;
then
A31: x in M by AFF_1:def 2;
A32: b in M by AFF_1:15;
A33: a in M by AFF_1:15;
A34: M // K by A1,A28,AFF_1:def 5;
then x,y // M by A9,AFF_1:43;
then y in M by A30,A31,AFF_1:23;
hence thesis by A4,A5,A6,A7,A8,A10,A11,A12,A28,A29,A33,A32,A34,A31,Th7;
end;
A35: a=b implies x=y
proof
set M=Line(x,y);
A36: x in M by AFF_1:15;
assume a=b;
then p9,x // p9,y by A2,A5,A7,A8,AFF_1:5;
then LIN p9,x,y by AFF_1:def 1;
then LIN x,y,p9 by AFF_1:6;
then
A37: p9 in M by AFF_1:def 2;
assume x<>y;
then M // K by A9,AFF_1:def 5;
hence contradiction by A3,A6,A36,A37,AFF_1:45;
end;
now
assume
A38: p=q;
p9=q9
proof
p9,x // q9,x by A2,A5,A7,A12,A38,AFF_1:5;
then x,p9 // x,q9 by AFF_1:4;
then LIN x,p9,q9 by AFF_1:def 1;
then
A39: LIN p9,q9,x by AFF_1:6;
assume p9<>q9;
hence contradiction by A1,A3,A6,A11,A39,AFF_1:25,26;
end;
hence thesis by A8,A38;
end;
hence thesis by A12,A35,A14,A26;
end;
Lm22: a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in
K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s
// K & q,b // q9,s implies s=y
proof
assume that
A1: a,b // K and
A2: not a in K and
A3: not x in K and
A4: AFP is Moufangian and
A5: p in K and
A6: p9 in K and
A7: p,a // p9,x and
A8: p,b // p9,y and
A9: x,y // K and
A10: q in K and
A11: q9 in K and
A12: q,a // q9,x and
A13: x,s // K and
A14: q,b // q9,s;
A15: not b in K by A1,A2,AFF_1:35;
q,b // q9,y by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,Lm21;
then q9,s // q9,y by A10,A14,A15,AFF_1:5;
then LIN q9,s,y by AFF_1:def 1;
then
A16: LIN y,s,q9 by AFF_1:6;
assume
A17: not thesis;
K is being_line by A1,AFF_1:26; then
consider M such that
A18: x in M and
A19: K // M by AFF_1:49;
A20: M is being_line by A19,AFF_1:36;
x,s // M by A13,A19,AFF_1:43;
then
A21: s in M by A18,A20,AFF_1:23;
x,y // M by A9,A19,AFF_1:43;
then y in M by A18,A20,AFF_1:23;
then M=Line(y,s) by A17,A20,A21,AFF_1:24;
then q9 in M by A16,AFF_1:def 2;
hence contradiction by A3,A11,A18,A19,AFF_1:45;
end;
Lm23: a,b // K & not a in K & AFP is Moufangian & ( x in K & x=y or (not x in
K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)) & ( r
in K & r=y or (not r in K & ex p,p9 st p in K & p9 in K & p,a // p9,r & p,b //
p9,y & r,y // K)) implies x=r
proof
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian and
A4: x in K & x=y or (not x in K & ex p,p9 st p in K & p9 in K & p,a //
p9,x & p,b // p9,y & x,y // K) and
A5: r in K & r=y or (not r in K & ex p,p9 st p in K & p9 in K & p,a //
p9,r & p,b // p9,y & r,y // K);
A6: y in K & y=r or (not y in K & ex p,p9 st p in K & p9 in K & p,b // p9,y
& p,a // p9,r & y,r // K) by A1,A2,A5,Lm18;
A7: b,a // K by A1,AFF_1:34;
A8: not b in K by A1,A2,AFF_1:35;
y in K & y=x or (not y in K & ex p,p9 st p in K & p9 in K & p,b // p9,y
& p,a // p9,x & y,x // K) by A1,A2,A4,Lm18;
hence thesis by A3,A7,A8,A6,Lm22;
end;
Lm24: a,b // K & not a in K & AFP is Moufangian implies ex f st for x,y holds
(f.x=y iff ( x in K & x=y or (not x in K & ex p,p9 st p in K & p9 in K & p,a //
p9,x & p,b // p9,y & x,y // K)))
proof
defpred P[Element of AFP, Element of AFP] means (($1 in K & $1=$2) or (not
$1 in K & ex p,p9 st p in K & p9 in K & p,a // p9,$1 & p,b // p9,$2 & $1,$2 //
K));
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian;
A4: for x,y,s st P[x,y] & P[x,s] holds y=s by A1,A2,A3,Lm22;
A5: for y ex x st P[x,y] by A1,A2,Lm20;
A6: for x ex y st P[x,y] by A1,A2,Lm19;
A7: for x,y,r st P[x,y] & P[r,y] holds x=r by A1,A2,A3,Lm23;
ex f st for x,y holds (f.x=y iff P[x,y]) from TRANSGEO:sch 1(A6,A5, A7,
A4);
hence thesis;
end;
Lm25: (a,b // K & not a in K & for x,y holds (f.x=y iff ( x in K & x=y or (not
x in K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))))
implies f.a=b
proof
assume that
A1: a,b // K and
A2: not a in K;
consider p,q such that
A3: p in K and
q in K and
p<>q by A1,AFF_1:19,26;
A4: p,b // p,b by AFF_1:2;
assume
A5: for x,y holds (f.x=y iff ( x in K & x=y or (not x in K & ex p,p9 st
p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)));
p,a // p,a by AFF_1:2;
hence thesis by A1,A2,A5,A3,A4;
end;
Lm26: (a,b // K & for x,y holds (f.x=y iff ( x in K & x=y or (not x in K & ex
p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)))) implies for
x holds x,f.x // K
proof
assume that
A1: a,b // K and
A2: for x,y holds (f.x=y iff ( x in K & x=y or (not x in K & ex p,p9 st
p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)));
let x;
set y=f.x;
A3: K is being_line by A1,AFF_1:26;
A4: now
assume x in K;
then y=x by A2;
hence thesis by A3,AFF_1:33;
end;
now
assume not x in K;
then
ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K by A2;
hence thesis;
end;
hence thesis by A4;
end;
Lm27: (a,b // K & not a in K & for x,y holds (f.x=y iff ( x in K & x=y or (not
x in K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))))
implies f is collineation
proof
assume that
A1: a,b // K and
A2: not a in K and
A3: for x,y holds (f.x=y iff ( x in K & x=y or (not x in K & ex p,p9 st
p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K)));
A4: K is being_line by A1,AFF_1:26;
A5: not b in K by A1,A2,AFF_1:35;
for A st A is being_line holds f.:A is being_line
proof
let A such that
A6: A is being_line;
set B9=f.:A;
A7: now
assume that
A8: A // K and
A9: A<>K;
now
let x such that
A10: x in A;
consider y such that
A11: f.y=x by TRANSGEO:1;
y in K & y=x or (not y in K & ex p,p9 st p in K & p9 in K & p,a
// p9,y & p,b // p9,x & y,x // K) by A3,A11;
then x,y // K by A8,A9,A10,AFF_1:34,45;
then x,y // A by A8,AFF_1:43;
then y in A by A6,A10,AFF_1:23;
hence x in B9 by A11,TRANSGEO:91;
end;
then
A12: A c= B9 by SUBSET_1:2;
now
let y;
assume y in B9;
then consider x such that
A13: x in A and
A14: y = f.x by TRANSGEO:91;
not x in K by A8,A9,A13,AFF_1:45;
then ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y //
K by A3,A14;
then x,y // A by A8,AFF_1:43;
hence y in A by A6,A13,AFF_1:23;
end;
then B9 c= A by SUBSET_1:2;
hence thesis by A6,A12,XBOOLE_0:def 10;
end;
A15: now
K is being_line by A1,AFF_1:26; then
consider M such that
A16: a in M and
A17: K // M by AFF_1:49;
A18: M is being_line by A17,AFF_1:36;
consider A9 such that
A19: a in A9 and
A20: A // A9 by A6,AFF_1:49;
A21: A9 is being_line by A20,AFF_1:36;
assume that
A22: not A // K and
A23: A<>K;
consider p such that
A24: p in A and
A25: p in K by A4,A6,A22,AFF_1:58;
not A9 // K by A22,A20,AFF_1:44;
then consider q such that
A26: q in A9 and
A27: q in K by A4,A21,AFF_1:58;
set C9=Line(q,b);
A28: q in C9 by AFF_1:15;
a,b // M by A1,A17,AFF_1:43;
then b in M by A16,A18,AFF_1:23;
then q<>b by A2,A16,A17,A27,AFF_1:45;
then C9 is being_line by AFF_1:def 3;
then consider C such that
A29: p in C and
A30: C9 // C by AFF_1:49;
A31: b in C9 by AFF_1:15;
A32: C is being_line by A30,AFF_1:36;
now
let y such that
A33: y in C;
A34: now
A35: q,b // p,y by A28,A31,A29,A30,A33,AFF_1:39;
K is being_line by A1,AFF_1:26; then
consider N such that
A36: y in N and
A37: K // N by AFF_1:49;
A38: N is being_line by A37,AFF_1:36;
not N // A by A22,A37,AFF_1:44;
then consider x such that
A39: x in N and
A40: x in A by A6,A38,AFF_1:58;
A41: x,y // K by A36,A37,A39,AFF_1:40;
assume
A42: y<>p;
A43: not x in K
proof
assume x in K;
then y in K by A36,A37,A39,AFF_1:45;
then C9 // K by A4,A25,A29,A30,A32,A33,A42,AFF_1:18;
hence contradiction by A5,A27,A28,A31,AFF_1:45;
end;
q,a // p,x by A24,A19,A20,A26,A40,AFF_1:39;
then y=f.x by A3,A25,A27,A43,A35,A41;
hence y in B9 by A40,TRANSGEO:91;
end;
now
assume
A44: y=p;
f.p=p by A3,A25;
hence y in B9 by A24,A44,TRANSGEO:91;
end;
hence y in B9 by A34;
end;
then
A45: C c= B9 by SUBSET_1:2;
now
let y;
assume y in B9;
then consider x such that
A46: x in A and
A47: y=f.x by TRANSGEO:91;
now
K is being_line by A1,AFF_1:26; then
consider N such that
A48: x in N and
A49: K // N by AFF_1:49;
A50: not C // N
proof
assume C // N;
then C9 // N by A30,AFF_1:44;
then
A51: C9 // K by A49,AFF_1:44;
q in C9 by AFF_1:15;
then C9=K by A27,A51,AFF_1:45;
hence contradiction by A5,AFF_1:15;
end;
N is being_line by A49,AFF_1:36;
then consider z such that
A52: z in C and
A53: z in N by A32,A50,AFF_1:58;
A54: x,z // K by A48,A49,A53,AFF_1:40;
assume x<>p;
then
A55: not x in K by A4,A6,A23,A24,A25,A46,AFF_1:18;
A56: q,a // p,x by A24,A19,A20,A26,A46,AFF_1:39;
q,b // p,z by A28,A31,A29,A30,A52,AFF_1:39;
hence y in C by A3,A25,A27,A47,A55,A52,A56,A54;
end;
hence y in C by A3,A25,A29,A47;
end;
then B9 c= C by SUBSET_1:2;
hence thesis by A32,A45,XBOOLE_0:def 10;
end;
now
assume
A57: A=K;
now
let y;
assume y in B9;
then ex x st x in A & y=f.x by TRANSGEO:91;
hence y in A by A3,A57;
end;
then
A58: B9 c= A by SUBSET_1:2;
now
let x such that
A59: x in A;
set y=f.x;
y in B9 by A59,TRANSGEO:90;
hence x in B9 by A3,A57,A59;
end;
then A c= B9 by SUBSET_1:2;
hence thesis by A6,A58,XBOOLE_0:def 10;
end;
hence thesis by A7,A15;
end;
hence thesis by TRANSGEO:96;
end;
Lm28: (a,b // K & not a in K & for x,y holds (f.x=y iff ( x in K & x=y or (not
x in K & ex p,p9 st p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))))
implies f is_Sc K
by Lm26,AFF_1:26,Lm27;
theorem Th8:
a,b // K & not a in K & AFP is Moufangian implies ex f st f is_Sc K & f.a=b
proof
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian;
consider f such that
A4: for x,y holds (f.x=y iff ( x in K & x=y or (not x in K & ex p,p9 st
p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K))) by A1,A2,A3,Lm24;
A5: f.a=b by A1,A2,A4,Lm25;
f is_Sc K by A1,A2,A4,Lm28;
hence thesis by A5;
end;
theorem
AFP is Moufangian iff for a,b,K st a,b // K & not a in K ex f st f
is_Sc K & f.a=b by Th6,Th8;