:: Translations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received June 12, 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, VECTSP_1, ANALOAF, FUNCT_2, STRUCT_0, TRANSGEO,
FUNCT_1, AFF_2, INCSP_1, AFF_1, RELAT_1;
notations PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, TRANSGEO;
constructors RELAT_2, PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0;
requirements SUBSET, BOOLE;
theorems FUNCT_2, TRANSGEO, AFF_1, AFF_2, FUNCT_1, DIRAF, RELAT_1;
schemes TRANSGEO;
begin
reserve AS for AffinSpace,
a,b,c,d,p,q,r,s,x for Element of AS;
definition
let AS;
attr AS is Fanoian means
for a,b,c,d st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,c;
end;
Lm1: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p implies ex x st LIN p,a,x
& p<>x & a<>x
proof
assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p;
a,b // a,c by A1,AFF_1:def 1;
then b,a // a,c by AFF_1:4;
then consider x such that
A6: p,a // a,x and
A7: p,b // c,x by A2,DIRAF:40;
A8: now
assume p = x;
then p,b // p,c by A7,AFF_1:4;
then LIN p,b,c by AFF_1:def 1;
then
A9: LIN b,c,p by AFF_1:6;
LIN b,c,a & LIN b,c,b by A1,AFF_1:6,7;
hence contradiction by A4,A5,A9,AFF_1:8;
end;
A10: now
assume a = x;
then
A11: p,b // a,c by A7,AFF_1:4;
a,b // a,c by A1,AFF_1:def 1;
then a,b // p,b by A3,A11,AFF_1:5;
then b,a // b,p by AFF_1:4;
then LIN b,a,p by AFF_1:def 1;
hence contradiction by A5,AFF_1:6;
end;
a,p // a,x by A6,AFF_1:4;
then LIN a,p,x by AFF_1:def 1;
then LIN p,a,x by AFF_1:6;
hence thesis by A8,A10;
end;
Lm2: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p & LIN a,b,q implies ex x
st LIN p,q,x & p<>x & q<>x
proof
assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p and
A6: LIN a,b,q;
A7: now
assume that
A8: q = c and
q<>a and
q<>b;
A9: now
assume
A10: LIN q,a,p;
LIN c,a,b & LIN c,a,a by A1,AFF_1:6,7;
hence contradiction by A3,A5,A8,A10,AFF_1:8;
end;
LIN q,a,b by A6,AFF_1:6;
hence thesis by A2,A3,A4,A8,A9,Lm1;
end;
A11: now
assume that
A12: q<>a and
A13: q<>b and
q<>c;
A14: now
assume LIN q,a,p;
then LIN a,q,p by AFF_1:6;
then
A15: a,q // a,p by AFF_1:def 1;
LIN a,q,b by A6,AFF_1:6;
then a,q // a,b by AFF_1:def 1;
then a,b // a,p by A12,A15,AFF_1:5;
hence contradiction by A5,AFF_1:def 1;
end;
LIN q,a,b by A6,AFF_1:6;
hence thesis by A2,A12,A13,A14,Lm1;
end;
now
assume that
A16: q = b and
q<>a and
q<>c;
LIN q,a,c & not LIN q,a,p by A1,A5,A16,AFF_1:6;
hence thesis by A2,A3,A4,A16,Lm1;
end;
hence thesis by A1,A2,A3,A4,A5,A7,A11,Lm1;
end;
Lm3: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p & p,q // a,b implies ex x
st LIN p,q,x & p<>x & q<>x
proof
assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p and
A6: p,q // a,b;
A7: b<>q
proof
assume b = q;
then b,p // b,a by A6,AFF_1:4;
then LIN b,p,a by AFF_1:def 1;
hence contradiction by A5,AFF_1:6;
end;
A8: a<>q
proof
assume a = q;
then a,p // a,b by A6,AFF_1:4;
then LIN a,p,b by AFF_1:def 1;
hence contradiction by A5,AFF_1:6;
end;
A9: not LIN a,b,q
proof
assume
A10: LIN a,b,q;
then a,b // a,q by AFF_1:def 1;
then p,q // a,q by A2,A6,AFF_1:5;
then q,p // q,a by AFF_1:4;
then LIN q,p,a by AFF_1:def 1;
then
A11: LIN q,a,p by AFF_1:6;
A12: LIN q,a,a by AFF_1:7;
LIN q,a,b by A10,AFF_1:6;
hence contradiction by A5,A8,A11,A12,AFF_1:8;
end;
consider r such that
A13: b,c // q,r and
A14: b,q // c,r by DIRAF:40;
LIN b,a,c by A1,AFF_1:6;
then b,a // b,c by AFF_1:def 1;
then b,a // q,r by A4,A13,AFF_1:5;
then a,b // q,r by AFF_1:4;
then p,q // q,r by A2,A6,AFF_1:5;
then q,p // q,r by AFF_1:4;
then LIN q,p,r by AFF_1:def 1;
then
A15: LIN p,q,r by AFF_1:6;
A16: not LIN a,c,p
proof
assume
A17: LIN a,c,p;
LIN a,c,b & LIN a,c,a by A1,AFF_1:6,7;
hence contradiction by A3,A5,A17,AFF_1:8;
end;
A18: now
consider s such that
A19: b,a // q,s and
A20: b,q // a,s by DIRAF:40;
A21: q<>s
proof
assume q = s;
then q,b // q,a by A20,AFF_1:4;
then LIN q,b,a by AFF_1:def 1;
hence contradiction by A9,AFF_1:6;
end;
assume
A22: p = r;
A23: now
assume p = s;
then a,p // c,p by A7,A14,A22,A20,AFF_1:5;
then p,a // p,c by AFF_1:4;
then LIN p,a,c by AFF_1:def 1;
hence contradiction by A16,AFF_1:6;
end;
a,b // q,s by A19,AFF_1:4;
then p,q // q,s by A2,A6,AFF_1:5;
then q,p // q,s by AFF_1:4;
then LIN q,p,s by AFF_1:def 1;
then LIN p,q,s by AFF_1:6;
hence thesis by A23,A21;
end;
q<>r
proof
assume q = r;
then q,b // q,c by A14,AFF_1:4;
then LIN q,b,c by AFF_1:def 1;
then
A24: LIN b,c,q by AFF_1:6;
LIN b,c,a & LIN b,c,b by A1,AFF_1:6,7;
hence contradiction by A4,A9,A24,AFF_1:8;
end;
hence thesis by A15,A18;
end;
theorem Th1:
(ex a,b,c st LIN a,b,c & a<>b & a<>c & b<>c) implies for p,q
holds ex r st LIN p,q,r & p<>r & q<>r
proof
given a,b,c such that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c;
let p,q;
A5: now
assume that
A6: LIN a,b,p and
A7: LIN a,b,q;
A8: LIN a,b,b by AFF_1:7;
A9: LIN a,b,a by AFF_1:7;
now
assume
A10: p = c or q = c;
now
assume p <> a or q <> b;
A11: now
assume that
A12: p = c and
A13: p<>a;
q = b implies thesis by A1,A2,A9,A8,A12,A13,AFF_1:8;
hence thesis by A1,A2,A4,A7,A8,A12,AFF_1:8;
end;
now
assume that
A14: q = c and
q<>b;
p = b implies thesis by A1,A2,A3,A9,A8,A14,AFF_1:8;
hence thesis by A1,A2,A4,A6,A8,A14,AFF_1:8;
end;
hence thesis by A3,A4,A10,A11;
end;
hence thesis by A1,A3,A4;
end;
hence thesis by A1,A2,A6,A7,AFF_1:8;
end;
A15: now
assume that
A16: not LIN a,b,p and
not LIN a,b,q;
now
consider p9 being Element of AS such that
A17: a,b // p,p9 and
A18: p<>p9 by DIRAF:40;
assume
A19: not p,q // a,b;
A20: not LIN p,p9,q
proof
assume LIN p,p9,q;
then p,p9 // p,q by AFF_1:def 1;
hence contradiction by A19,A17,A18,AFF_1:5;
end;
p,p9 // a,b by A17,AFF_1:4;
then
ex p99 being Element of AS st LIN p,p9,p99 & p<>p99 & p9<>p99 by A1,A2,A3
,A4,A16,Lm3;
then consider r such that
A21: LIN q,p,r and
A22: q<>r & p<>r by A18,A20,Lm1;
LIN p,q,r by A21,AFF_1:6;
hence thesis by A22;
end;
hence thesis by A1,A2,A3,A4,A16,Lm3;
end;
now
assume ( not LIN a,b,q)& LIN a,b,p;
then consider x such that
A23: LIN q,p,x and
A24: q<>x & p<>x by A1,A2,A3,A4,Lm2;
LIN p,q,x by A23,AFF_1:6;
hence thesis by A24;
end;
hence thesis by A1,A2,A3,A4,A5,A15,Lm2;
end;
reserve AFP for AffinPlane,
a,a9,b,b9,c,c9,d,p,p9,q,q9,r,x,x9,y,y9,z for Element of AFP,
A,C,P for Subset of AFP,
f,g,h,f1,f2 for Permutation of the carrier of AFP;
theorem Th2:
AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c implies
ex p st LIN b,c,p & LIN a,d,p
proof
assume ( for a,b,c,d st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,
c)& a,b // c,d & a,c // b,d & not LIN a,b,c;
then not a,d // b,c;
then ex p st LIN a,d,p & LIN b,c,p by AFF_1:60;
hence thesis;
end;
Lm4: not LIN a,b,x & a,b // x,y & x<>y implies not LIN x,y,a & not LIN b,a,y &
not LIN y,x,b
proof
assume that
A1: not LIN a,b,x and
A2: a,b // x,y and
A3: x<>y;
thus not LIN x,y,a
proof
A4: LIN x,y,x by AFF_1:7;
assume
A5: LIN x,y,a;
x,y // a,b by A2,AFF_1:4;
then LIN x,y,b by A3,A5,AFF_1:9;
hence contradiction by A1,A3,A5,A4,AFF_1:8;
end;
thus not LIN b,a,y
proof
assume
A6: LIN b,a,y;
b,a // y,x & b<>a by A1,A2,AFF_1:4,7;
then LIN b,a,x by A6,AFF_1:9;
hence contradiction by A1,AFF_1:6;
end;
thus not LIN y,x,b
proof
A7: LIN y,x,x by AFF_1:7;
assume
A8: LIN y,x,b;
y,x // b,a by A2,AFF_1:4;
then LIN y,x,a by A3,A8,AFF_1:9;
hence contradiction by A1,A3,A8,A7,AFF_1:8;
end;
end;
Lm5: not LIN a,b,x & a,b // x,y & a,x // b,y implies not LIN x,y,a & not LIN b
,a,y & not LIN y,x,b
proof
assume that
A1: not LIN a,b,x and
A2: a,b // x,y and
A3: a,x // b,y;
x<>y
proof
assume x=y;
then x,a // x,b by A3,AFF_1:4;
then LIN x,a,b by AFF_1:def 1;
hence contradiction by A1,AFF_1:6;
end;
hence thesis by A1,A2,Lm4;
end;
theorem Th3:
f is translation & not LIN a,f.a,x & a,f.a // x,y & a,x // f.a,y
implies y=f.x
proof
assume
A1: f is translation;
then
A2: f is dilatation by TRANSGEO:def 11;
then
A3: a,x // f.a,f.x by TRANSGEO:68;
assume
A4: ( not LIN a,f.a,x)& a,f.a // x,y & a,x // f.a,y;
a,f.a // x,f.x by A1,A2,TRANSGEO:82;
hence thesis by A4,A3,TRANSGEO:80;
end;
theorem Th4:
AFP is translational iff for a,a9,b,c,b9,c9 st not LIN a,a9,b &
not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9
holds b,c // b9,c9
proof
thus AFP is translational implies for a,a9,b,c,b9,c9 st not LIN a,a9,b & not
LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,
c // b9,c9
proof
assume
A1: AFP is translational;
let a,a9,b,c,b9,c9;
assume that
A2: not LIN a,a9,b and
A3: not LIN a,a9,c and
A4: a,a9 // b,b9 and
A5: a,a9 // c,c9 and
A6: a,b // a9,b9 and
A7: a,c // a9,c9;
set A=Line(a,a9), P=Line(b,b9), C=Line(c,c9);
A8: a in A & a9 in A by AFF_1:15;
A9: c <>c9
proof
assume c = c9;
then c,a // c,a9 by A7,AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
hence contradiction by A3,AFF_1:6;
end;
then
A10: C is being_line by AFF_1:def 3;
A11: b<>b9
proof
assume b=b9;
then b,a // b,a9 by A6,AFF_1:4;
then LIN b,a,a9 by AFF_1:def 1;
hence contradiction by A2,AFF_1:6;
end;
then
A12: P is being_line by AFF_1:def 3;
A13: a<>a9 by A2,AFF_1:7;
then
A14: A is being_line by AFF_1:def 3;
A15: c in C by AFF_1:15;
then
A16: A<>C by A3,A8,A14,AFF_1:21;
A17: A // P by A4,A13,A11,AFF_1:37;
A18: b9 in P & c9 in C by AFF_1:15;
A19: A // C by A5,A13,A9,AFF_1:37;
A20: b in P by AFF_1:15;
then A<>P by A2,A8,A14,AFF_1:21;
hence thesis by A1,A6,A7,A8,A20,A15,A18,A14,A12,A10,A17,A19,A16,
AFF_2:def 11;
end;
assume
A21: for a,a9,b,c,b9,c9 st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,
b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9;
now
let A,P,C,a,b,c,a9,b9,c9;
assume that
A22: A // P and
A23: A // C and
A24: a in A and
A25: a9 in A and
A26: b in P and
A27: b9 in P and
A28: c in C and
A29: c9 in C and
A30: A is being_line and
A31: P is being_line and
A32: C is being_line and
A33: A<>P and
A34: A<>C and
A35: a,b // a9,b9 and
A36: a,c // a9,c9;
A37: a,a9 // b,b9 & a,a9 // c,c9 by A22,A23,A24,A25,A26,A27,A28,A29,AFF_1:39;
A38: now
assume
A39: a<>a9;
A40: not LIN a,a9,c
proof
assume LIN a,a9,c;
then c in A by A24,A25,A30,A39,AFF_1:25;
hence contradiction by A23,A28,A34,AFF_1:45;
end;
not LIN a,a9,b
proof
assume LIN a,a9,b;
then b in A by A24,A25,A30,A39,AFF_1:25;
hence contradiction by A22,A26,A33,AFF_1:45;
end;
hence b,c // b9,c9 by A21,A35,A36,A37,A40;
end;
now
assume
A41: a=a9;
then LIN a,c,c9 by A36,AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then
A42: c = c9 or a in C by A28,A29,A32,AFF_1:25;
LIN a,b,b9 by A35,A41,AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b=b9 or a in P by A26,A27,A31,AFF_1:25;
hence b,c // b9,c9 by A22,A23,A24,A33,A34,A42,AFF_1:2,45;
end;
hence b,c // b9,c9 by A38;
end;
hence thesis by AFF_2:def 11;
end;
theorem Th5:
ex f st f is translation & f.a=a
proof
take id the carrier of AFP;
thus thesis by TRANSGEO:81;
end;
Lm6: a<>b implies ex y st ( not LIN a,b,x & a,b // x,y & a,x // b,y or (LIN a,
b,x & ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q
,y))
proof
assume
A1: a<>b;
A2: now
assume
A3: LIN a,b,x;
consider p such that
A4: not LIN a,b,p by A1,AFF_1:13;
consider q such that
A5: a,b // p,q & a,p // b,q by DIRAF:40;
ex y st p,q // x,y & p,x // q,y by DIRAF:40;
hence thesis by A3,A4,A5;
end;
now
A6: ex y st a,b // x,y & a,x // b,y by DIRAF:40;
assume not LIN a,b,x;
hence thesis by A6;
end;
hence thesis by A2;
end;
Lm7: a<>b implies ex x st not LIN a,b,x & a,b // x,y & a,x // b,y or LIN a,b,x
& ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y
proof
assume
A1: a<>b;
A2: now
assume
A3: LIN a,b,y;
consider p such that
A4: not LIN a,b,p by A1,AFF_1:13;
consider q such that
A5: a,b // p,q and
A6: a,p // b,q by DIRAF:40;
A7: now
assume p=q;
then p,a // p,b by A6,AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A4,AFF_1:6;
end;
consider x such that
A8: q,p // y,x and
A9: q,y // p,x by DIRAF:40;
A10: p,x // q,y by A9,AFF_1:4;
A11: p,q // x,y by A8,AFF_1:4;
then a,b // x,y or p=q by A5,AFF_1:5;
then a,b // y,x by A7,AFF_1:4;
then LIN a,b,x by A1,A3,AFF_1:9;
hence thesis by A4,A5,A6,A11,A10;
end;
now
consider x such that
A12: b,a // y,x & b,y // a,x by DIRAF:40;
A13: a,b // x,y & a,x // b,y by A12,AFF_1:4;
assume not LIN a,b,y;
then not LIN b,a,y by AFF_1:6;
then not LIN a,b,x by A12,Lm5;
hence thesis by A13;
end;
hence thesis by A2;
end;
Lm8: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p
// b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9
& not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 implies y=y9
proof
assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9 and
A14: not LIN p,q,p9;
A15: p<>q
proof
assume p=q;
then p,a // p,b by A6,AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A12,AFF_1:6;
end;
A16: not LIN p,q,x
proof
assume
A17: LIN p,q,x;
then p,q // p,x by AFF_1:def 1;
then
A18: p,x // a,b by A4,A15,AFF_1:5;
a,b // a,x by A3,AFF_1:def 1;
then p,x // a,x by A2,A18,AFF_1:5;
then x,p // x,a by AFF_1:4;
then
A19: LIN x,p,a by AFF_1:def 1;
A20: LIN x,p,x & LIN a,x,b by A3,AFF_1:6,7;
A21: LIN x,p,p by AFF_1:7;
x<>a by A4,A6,A12,A17,Lm5;
then LIN x,p,b by A19,A20,AFF_1:11;
hence contradiction by A3,A12,A19,A21,AFF_1:8;
end;
A22: p,q // p9,q9 by A2,A4,A5,AFF_1:5;
then
A23: p9,q9 // x,y by A8,A15,AFF_1:5;
A24: p9<>q9
proof
assume p9=q9;
then p9,a // p9,b by A7,AFF_1:4;
then LIN p9,a,b by AFF_1:def 1;
hence contradiction by A13,AFF_1:6;
end;
A25: not LIN p9,q9,x
proof
assume
A26: LIN p9,q9,x;
then p9,q9 // p9,x by AFF_1:def 1;
then
A27: p9,x // a,b by A5,A24,AFF_1:5;
a,b // a,x by A3,AFF_1:def 1;
then p9,x // a,x by A2,A27,AFF_1:5;
then x,p9 // x,a by AFF_1:4;
then
A28: LIN x,p9,a by AFF_1:def 1;
A29: LIN x,p9,x & LIN a,x,b by A3,AFF_1:6,7;
A30: LIN x,p9,p9 by AFF_1:7;
x<>a by A5,A7,A13,A26,Lm5;
then LIN x,p9,b by A28,A29,AFF_1:11;
hence contradiction by A3,A13,A28,A30,AFF_1:8;
end;
p,p9 // q,q9 by A1,A4,A5,A6,A7,A12,A13,Th4;
then p9,x // q9,y by A1,A8,A10,A14,A22,A16,Th4;
hence thesis by A9,A11,A25,A23,TRANSGEO:80;
end;
theorem Th6:
(for p,q,r st p<>q & LIN p,q,r holds r = p or r = q) & a,b // p,q
& a,p // b,q & not LIN a,b,p implies a,q // b,p
proof
assume that
A1: for p,q,r st p<>q & LIN p,q,r holds r = p or r = q and
A2: a,b // p,q and
A3: a,p // b,q and
A4: not LIN a,b,p;
consider z such that
A5: q,p // a,z and
A6: q,a // p,z by DIRAF:40;
A7: p<>q
proof
assume p=q;
then p,a // p,b by A3,AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A4,AFF_1:6;
end;
A8: not LIN a,p,q
proof
A9: LIN p,q,p by AFF_1:7;
assume LIN a,p,q;
then
A10: LIN p,q,a by AFF_1:6;
p,q // a,b by A2,AFF_1:4;
then LIN p,q,b by A7,A10,AFF_1:9;
hence contradiction by A4,A7,A10,A9,AFF_1:8;
end;
A11: now
assume a=z;
then a,p // a,q by A6,AFF_1:4;
hence contradiction by A8,AFF_1:def 1;
end;
p,q // a,z by A5,AFF_1:4;
then a,b // a,z by A2,A7,AFF_1:5;
then
A12: LIN a,b,z by AFF_1:def 1;
a<>b by A4,AFF_1:7;
then a=z or b=z by A1,A12;
hence thesis by A6,A11,AFF_1:4;
end;
Lm9: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p
// b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9
& not LIN a,b,p & not LIN a,b,p9 implies y=y9
proof
assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9;
A14: p<>q
proof
assume p=q;
then p,a // p,b by A6,AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A12,AFF_1:6;
end;
then a,b // x,y by A4,A8,AFF_1:5;
then
A15: LIN a,b,y by A2,A3,AFF_1:9;
A16: not LIN p,q,x
proof
assume LIN p,q,x;
then p,q // p,x by AFF_1:def 1;
then a,b // p,x by A4,A14,AFF_1:5;
then a,b // x,p by AFF_1:4;
hence contradiction by A2,A3,A12,AFF_1:9;
end;
A17: now
assume x=y;
then x,p // x,q by A10,AFF_1:4;
then LIN x,p,q by AFF_1:def 1;
hence contradiction by A16,AFF_1:6;
end;
A18: p9<>q9
proof
assume p9=q9;
then p9,a // p9,b by A7,AFF_1:4;
then LIN p9,a,b by AFF_1:def 1;
hence contradiction by A13,AFF_1:6;
end;
A19: not LIN q,p,b
proof
A20: LIN q,p,p by AFF_1:7;
assume
A21: LIN q,p,b;
q,p // b,a by A4,AFF_1:4;
then LIN q,p,a by A14,A21,AFF_1:9;
hence contradiction by A12,A14,A21,A20,AFF_1:8;
end;
now
assume
A22: LIN p,q,p9;
p,q // p9,q9 by A2,A4,A5,AFF_1:5;
then
A23: LIN p,q,q9 by A14,A22,AFF_1:9;
A24: now
assume
A25: for x st LIN a,p,x holds x=a or x=p;
then
A26: for p,q,r st p<>q & LIN p,q,r holds r = p or r = q by Th1;
A27: now
assume
A28: q=p9;
A29: now
a,q // b,p by A4,A6,A12,A26,Th6;
then
A30: q,a // p,b by AFF_1:4;
A31: q,p // a,b by A4,AFF_1:4;
assume
A32: a=x;
then
A33: q,a // p,y9 & not LIN q,p,a by A11,A14,A18,A16,A23,A25,A28,Th1,
AFF_1:6;
b=y & q,p // a,y9 by A2,A9,A14,A18,A17,A15,A23,A25,A28,A32,Th1;
hence thesis by A31,A30,A33,TRANSGEO:80;
end;
now
A34: q,p // b,a & q,b // p,a by A4,A6,AFF_1:4;
assume
A35: b=x;
then
A36: q,b // p,y9 by A11,A14,A18,A23,A25,A28,Th1;
a=y & q,p // b,y9 by A2,A9,A14,A18,A17,A15,A23,A25,A28,A35,Th1;
hence thesis by A19,A34,A36,TRANSGEO:80;
end;
hence thesis by A2,A3,A25,A29,Th1;
end;
now
assume
A37: p=p9;
then q=q9 by A14,A18,A23,A25,Th1;
hence thesis by A8,A9,A10,A11,A16,A37,TRANSGEO:80;
end;
hence thesis by A14,A22,A25,A27,Th1;
end;
now
given p99 being Element of AFP such that
A38: LIN a,p,p99 and
A39: p99<>a and
A40: p99<>p;
A41: not LIN p,q,p99
proof
assume LIN p,q,p99;
then
A42: LIN p,p99,q by AFF_1:6;
LIN p,p99,p & LIN p,p99,a by A38,AFF_1:6,7;
then LIN p,q,a by A40,A42,AFF_1:8;
hence contradiction by A4,A6,A12,Lm5;
end;
A43: not LIN p9,q9,p99
proof
p,q // p9,q9 by A2,A4,A5,AFF_1:5;
then
A44: LIN p,q,q9 by A14,A22,AFF_1:9;
assume LIN p9,q9,p99;
hence contradiction by A18,A22,A41,A44,AFF_1:11;
end;
consider q99 being Element of AFP such that
A45: a,b // p99,q99 & a,p99 // b,q99 by DIRAF:40;
consider y99 being Element of AFP such that
A46: p99,q99 // x,y99 & p99,x // q99,y99 by DIRAF:40;
A47: not LIN a,b,p99
proof
assume LIN a,b,p99;
then
A48: LIN a,p99,b by AFF_1:6;
LIN a,p99,a & LIN a,p99,p by A38,AFF_1:6,7;
hence contradiction by A12,A39,A48,AFF_1:8;
end;
then y=y99 by A1,A2,A3,A4,A6,A8,A10,A12,A45,A46,A41,Lm8;
hence thesis by A1,A2,A3,A5,A7,A9,A11,A13,A45,A46,A43,A47,Lm8;
end;
hence thesis by A24;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Lm8;
end;
Lm10: a<>b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p
implies p<>q & LIN a,b,y
proof
assume that
A1: a<>b & LIN a,b,x and
A2: a,b // p,q and
A3: a,p // b,q and
A4: p,q // x,y and
A5: not LIN a,b,p;
thus p<>q
proof
assume p=q;
then p,a // p,b by A3,AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A5,AFF_1:6;
end;
then a,b // x,y by A2,A4,AFF_1:5;
hence thesis by A1,AFF_1:9;
end;
Lm11: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,
p // b,q & a,p9 // b,q9 & p,q // x,y & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9
,y & not LIN a,b,p & not LIN a,b,p9 implies x=x9
proof
assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p,x // q,y and
A10: p9,q9 // x9,y & p9,x9 // q9,y and
A11: not LIN a,b,p and
A12: not LIN a,b,p9;
A13: b,a // q,p & b,a // q9,p9 by A4,A5,AFF_1:4;
A14: b,q // a,p & b,q9 // a,p9 by A6,A7,AFF_1:4;
A15: q9,p9 // y,x9 & q9,y // p9,x9 by A10,AFF_1:4;
LIN a,b,y by A2,A3,A4,A6,A8,A11,Lm10;
then
A16: LIN b,a,y by AFF_1:6;
A17: q,p // y,x & q,y // p,x by A8,A9,AFF_1:4;
( not LIN b,a,q)& not LIN b,a,q9 by A4,A5,A6,A7,A11,A12,Lm5;
hence thesis by A1,A2,A16,A13,A14,A17,A15,Lm9;
end;
Lm12: AFP is translational & a<>b implies ex f st f is translation & f.a=b
proof
defpred X[Element of AFP,Element of AFP] means (not LIN a,b,$1 & a,b // $1,
$2 & a,$1 // b,$2) or (LIN a,b,$1 & (ex p,q st not LIN a,b,p & a,b // p,q & a,p
// b,q & p,q // $1,$2 & p,$1 // q,$2));
assume that
A1: AFP is translational and
A2: a<>b;
A3: ex y st X[x,y] by A2,Lm6;
A4: for x,y,x9 holds X[x,y] & X[x9,y] implies x=x9
proof
let x,y,x9;
assume that
A5: not LIN a,b,x & a,b // x,y & a,x // b,y or (LIN a,b,x & ex p,q st
not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y) and
A6: not LIN a,b,x9 & a,b // x9,y & a,x9 // b,y or (LIN a,b,x9 & ex p,
q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x9,y & p,x9 // q,y);
A7: now
assume
A8: LIN a,b,y;
A9: not (not LIN a,b,x9 & a,b // x9,y & a,x9 // b,y)
proof
assume that
A10: not LIN a,b,x9 and
A11: a,b // x9,y and
a,x9 // b,y;
a,b // y,x9 by A11,AFF_1:4;
hence contradiction by A2,A8,A10,AFF_1:9;
end;
not (not LIN a,b,x & a,b // x,y & a,x // b,y)
proof
assume that
A12: not LIN a,b,x and
A13: a,b // x,y and
a,x // b,y;
a,b // y,x by A13,AFF_1:4;
hence contradiction by A2,A8,A12,AFF_1:9;
end;
hence thesis by A1,A2,A5,A6,A9,Lm11;
end;
now
assume
A14: not LIN a,b,y;
then
A15: b,y // a,x9 by A2,A6,Lm10,AFF_1:4;
A16: b,y // a,x & b,a // y,x9 by A2,A5,A6,A14,Lm10,AFF_1:4;
( not LIN b,a,y)& b,a // y,x by A2,A5,A14,Lm5,Lm10,AFF_1:4;
hence thesis by A16,A15,TRANSGEO:80;
end;
hence thesis by A7;
end;
A17: ex x st X[x,y] by A2,Lm7;
A18: X[x,y] & X[x,y9] implies y=y9 by A1,A2,Lm9,TRANSGEO:80;
ex f st for x,y holds f.x=y iff X[x,y] from TRANSGEO:sch 1(A3,A17,A4,A18);
then consider f such that
A19: for x,y holds f.x=y iff not LIN a,b,x & a,b // x,y & a,x // b,y or
LIN a,b,x & ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,
x // q,y;
A20: a,b // x,f.x
proof
set y=f.x;
now
assume
A21: LIN a,b,x;
then consider p,q such that
A22: not LIN a,b,p and
A23: a,b // p,q and
A24: a,p // b,q and
A25: p,q // x,y and
p,x // q,y by A19;
p<>q by A2,A21,A22,A23,A24,A25,Lm10;
hence thesis by A23,A25,AFF_1:5;
end;
hence thesis by A19;
end;
for x,y holds x,y // f.x,f.y
proof
let x,y;
A26: now
A27: ex x9 st y,f.y // x,x9 & y,x // f.y,x9 by DIRAF:40;
assume that
A28: LIN a,b,x and
A29: not LIN a,b,y;
a,b // y,f.y & a,y // b,f.y by A19,A29;
then y,x // f.y,f.x by A19,A28,A29,A27;
hence thesis by AFF_1:4;
end;
A30: now
A31: ex y9 st x,f.x // y,y9 & x,y // f.x,y9 by DIRAF:40;
assume that
A32: not LIN a,b,x and
A33: LIN a,b,y;
a,b // x,f.x & a,x // b,f.x by A19,A32;
hence thesis by A19,A32,A33,A31;
end;
A34: now
assume
A35: LIN a,b,x & LIN a,b,y;
then LIN a,b,f.x & LIN a,b,f.y by A2,A20,AFF_1:9;
then
A36: a,b // f.x,f.y by AFF_1:10;
a,b // x,y by A35,AFF_1:10;
hence thesis by A2,A36,AFF_1:5;
end;
now
assume
A37: ( not LIN a,b,x)& not LIN a,b,y;
then
A38: a,b // x,f.x & a,b // y,f.y by A19;
a,x // b,f.x & a,y // b,f.y by A19,A37;
hence thesis by A1,A37,A38,Th4;
end;
hence thesis by A34,A26,A30;
end;
then
A39: f is dilatation by TRANSGEO:68;
A40: f.a=b
proof
A41: LIN a,b,a by AFF_1:7;
consider p such that
A42: not LIN a,b,p by A2,AFF_1:13;
consider q such that
A43: a,b // p,q & a,p // b,q by DIRAF:40;
p,a // q,b & p,q // a,b by A43,AFF_1:4;
hence thesis by A19,A42,A43,A41;
end;
x,f.x // y,f.y
proof
a,b // x,f.x & a,b // y,f.y by A20;
hence thesis by A2,AFF_1:5;
end;
then f is translation by A39,TRANSGEO:82;
hence thesis by A40;
end;
theorem Th7:
AFP is translational implies ex f st f is translation & f.a=b
proof
assume
A1: AFP is translational;
a=b implies thesis by Th5;
hence thesis by A1,Lm12;
end;
theorem
(for a,b ex f st f is translation & f.a=b) implies AFP is translational
proof
assume
A1: for a,b ex f st f is translation & f.a=b;
now
let a,a9,b,c,b9,c9;
consider f such that
A2: f is translation and
A3: f.a=a9 by A1;
A4: f is dilatation by A2,TRANSGEO:def 11;
assume ( not LIN a,a9,b)& not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 &
a,b // a9,b9 & a,c // a9,c9;
then b9=f.b & c9=f.c by A2,A3,Th3;
hence b,c // b9,c9 by A4,TRANSGEO:68;
end;
hence thesis by Th4;
end;
theorem Th9:
f is translation & g is translation & not LIN a,f.a,g.a implies f*g=g*f
proof
assume that
A1: f is translation and
A2: g is translation;
A3: g is dilatation by A2,TRANSGEO:def 11;
then
A4: a,f.a // g.a,g.(f.a) by TRANSGEO:68;
assume
A5: not LIN a,f.a,g.a;
a,g.a // f.a,g.(f.a) by A2,A3,TRANSGEO:82;
then f.(g.a)=g.(f.a) by A1,A5,A4,Th3;
then (f*g).a=g.(f.a) by FUNCT_2:15;
then
A6: (f*g).a=(g*f).a by FUNCT_2:15;
f*g is translation & g*f is translation by A1,A2,TRANSGEO:86;
hence thesis by A6,TRANSGEO:84;
end;
theorem Th10:
AFP is translational & f is translation & g is translation implies f*g=g*f
proof
assume that
A1: AFP is translational and
A2: f is translation and
A3: g is translation;
A4: g is dilatation by A3,TRANSGEO:def 11;
now
set a = the Element of AFP;
assume that
A5: f<>id the carrier of AFP and
A6: g<>id the carrier of AFP;
A7: a<>f.a by A2,A5,TRANSGEO:def 11;
A8: a<>g.a by A3,A6,TRANSGEO:def 11;
now
consider b such that
A9: not LIN a,f.a,b by A7,AFF_1:13;
consider h such that
A10: h is translation and
A11: h.a=b by A1,Th7;
A12: h *g is translation by A3,A10,TRANSGEO:86;
assume
A13: LIN a,f.a,g.a;
not LIN a,f.a,h.(g.a)
proof
A14: not LIN a,g.a,b
proof
assume
A15: LIN a,g.a,b;
LIN a,g.a,f.a & LIN a,g.a,a by A13,AFF_1:6,7;
hence contradiction by A8,A9,A15,AFF_1:8;
end;
then (g*h).a=(h*g).a by A3,A10,A11,Th9;
then (g*h).a=h.(g.a) by FUNCT_2:15;
then
A16: g.b=h.(g.a) by A11,FUNCT_2:15;
assume
A17: LIN a,f.a,h.(g.a);
a,g.a // b,g.b & a,b // g.a,g.b by A3,A4,TRANSGEO:68,82;
then LIN a,f.a,a & not LIN g.a,a,h.(g.a) by A14,A16,Lm5,AFF_1:7;
hence contradiction by A7,A13,A17,AFF_1:8;
end;
then
A18: not LIN a,f.a,(h*g).a by FUNCT_2:15;
h*(f*g)=(h*f)*g by RELAT_1:36
.=(f*h)*g by A2,A9,A10,A11,Th9
.=f*(h*g) by RELAT_1:36
.=(h*g)*f by A2,A12,A18,Th9
.=h*(g*f) by RELAT_1:36;
hence thesis by TRANSGEO:5;
end;
hence thesis by A2,A3,Th9;
end;
hence thesis by TRANSGEO:4;
end;
theorem Th11:
f is translation & g is translation & p,f.p // p,g.p implies p,f
.p // p,(f*g).p
proof
assume that
A1: f is translation and
A2: g is translation and
A3: p,f.p // p,g.p;
A4: f is dilatation by A1,TRANSGEO:def 11;
A5: now
assume g<>id the carrier of AFP;
then
A6: g.p<>p by A2,TRANSGEO:def 11;
p,g.p // f.p,f.(g.p) by A4,TRANSGEO:68;
then p,f.p // f.p,f.(g.p) by A3,A6,AFF_1:5;
then f.p,p // f.p,f.(g.p) by AFF_1:4;
then LIN f.p,p,f.(g.p) by AFF_1:def 1;
then LIN p,f.p,f.(g.p) by AFF_1:6;
then p,f.p // p,f.(g.p) by AFF_1:def 1;
hence thesis by FUNCT_2:15;
end;
now
assume g=id the carrier of AFP;
then f*g=f by FUNCT_2:17;
hence thesis by AFF_1:2;
end;
hence thesis by A5;
end;
theorem
AFP is Fanoian & AFP is translational & f is translation implies ex g
st g is translation & g*g=f
proof
assume that
A1: AFP is Fanoian and
A2: AFP is translational and
A3: f is translation;
A4: now
set a = the Element of AFP;
set b=f.a;
assume f<>id the carrier of AFP;
then a<>b by A3,TRANSGEO:def 11;
then consider c such that
A5: not LIN a,b,c by AFF_1:13;
consider d such that
A6: c,b // a,d and
A7: c,a // b,d by DIRAF:40;
not LIN c,b,a by A5,AFF_1:6;
then consider p such that
A8: LIN b,a,p and
A9: LIN c,d,p by A1,A6,A7,Th2;
consider f1 being Permutation of the carrier of AFP such that
A10: f1 is translation and
A11: f1.p=a by A2,Th7;
consider f2 being Permutation of the carrier of AFP such that
A12: f2 is translation and
A13: f2.p=b by A2,Th7;
A14: f1*f2 is translation by A10,A12,TRANSGEO:86;
A15: LIN p,c,d by A9,AFF_1:6;
then
A16: p,c // p,d by AFF_1:def 1;
A17: now
assume p,c // p,a;
then LIN p,c,a by AFF_1:def 1;
then
A18: LIN p,a,c by AFF_1:6;
LIN p,a,a & LIN p,a,b by A8,AFF_1:6,7;
then p=a by A5,A18,AFF_1:8;
then a,c // c,b or a=d by A6,A16,AFF_1:5;
then c,a // c,b or a=d by AFF_1:4;
then LIN c,a,b or a=d by AFF_1:def 1;
then a,c // a,b by A5,A7,AFF_1:4,6;
then LIN a,c,b by AFF_1:def 1;
hence contradiction by A5,AFF_1:6;
end;
consider f3 being Permutation of the carrier of AFP such that
A19: f3 is translation and
A20: f3.p=c by A2,Th7;
(f3)" is translation by A19,TRANSGEO:85;
then
A21: f1*(f3)" is translation by A10,TRANSGEO:86;
LIN p,a,b by A8,AFF_1:6;
then p,f1.p // p,f2.p by A11,A13,AFF_1:def 1;
then
A22: p,a // p,(f1*f2).p by A10,A11,A12,Th11;
consider f4 being Permutation of the carrier of AFP such that
A23: f4 is translation and
A24: f4.p=d by A2,Th7;
f4.((f2)".b)=f4.p by A13,TRANSGEO:2;
then
A25: (f4*f2").b=d by A24,FUNCT_2:15;
consider h such that
A26: h is translation and
A27: h.c = a by A2,Th7;
not LIN c,a,b by A5,AFF_1:6;
then
A28: h.b=d by A6,A7,A26,A27,Th3;
f1.((f3)".c)=f1.p by A20,TRANSGEO:2;
then (f1*(f3)").c = a by A11,FUNCT_2:15;
then
A29: f1*(f3)"=h by A26,A27,A21,TRANSGEO:84;
A30: (f2)" is translation by A12,TRANSGEO:85;
then f4*f2" is translation by A23,TRANSGEO:86;
then f1*f3"=f4*f2" by A26,A28,A29,A25,TRANSGEO:84;
then f1*(f3"*f3)=(f4*f2")*f3 by RELAT_1:36;
then f1*(id the carrier of AFP)=(f4*f2")*f3 by FUNCT_2:61;
then f1=(f4*f2")*f3 by FUNCT_2:17
.=f4*(f2"*f3) by RELAT_1:36
.=f4*(f3*f2") by A2,A19,A30,Th10
.=(f4*f3)*f2" by RELAT_1:36;
then
A31: f1*f2=(f4*f3)*(f2"*f2) by RELAT_1:36
.=(f4*f3)*(id the carrier of AFP) by FUNCT_2:61
.=f4*f3 by FUNCT_2:17;
p,f3.p // p,f4.p by A20,A24,A15,AFF_1:def 1;
then p,c // p,(f3*f4).p by A19,A20,A23,Th11;
then p,c // p,(f1*f2).p by A2,A19,A23,A31,Th10;
then p=(f1*f2).p by A22,A17,AFF_1:5;
then f1"*(f1*f2)=f1"*(id the carrier of AFP) by A14,TRANSGEO:def 11;
then (f1"*f1)*f2=f1"*(id the carrier of AFP) by RELAT_1:36;
then (id the carrier of AFP)*f2=f1"*(id the carrier of AFP) by FUNCT_2:61;
then f2=f1"*(id the carrier of AFP) by FUNCT_2:17;
then
A32: (f2*f2).a=(f2*f1").a by FUNCT_2:17
.=f2.(f1".a) by FUNCT_2:15
.=b by A11,A13,TRANSGEO:2;
f2*f2 is translation by A12,TRANSGEO:86;
hence thesis by A3,A12,A32,TRANSGEO:84;
end;
now
set g=id the carrier of AFP;
A33: g is translation & g*g=id the carrier of AFP by FUNCT_2:17,TRANSGEO:81;
assume f=id the carrier of AFP;
hence thesis by A33;
end;
hence thesis by A4;
end;
theorem Th13:
AFP is Fanoian & f is translation & f*f=id the carrier of AFP
implies f=id the carrier of AFP
proof
set a = the Element of AFP;
assume that
A1: AFP is Fanoian and
A2: f is translation and
A3: f*f=id the carrier of AFP;
assume f<>id the carrier of AFP;
then a<>f.a by A2,TRANSGEO:def 11;
then consider b such that
A4: not LIN a,f.a,b by AFF_1:13;
A5: f is dilatation by A2,TRANSGEO:def 11;
then
A6: a,b // f.a,f.b by TRANSGEO:68;
f.b,a // f.(f.b),f.a by A5,TRANSGEO:68;
then f.b,a // (f*f).b,f.a by FUNCT_2:15;
then f.b,a // b,f.a by A3;
then
A7: a,f.b // f.a,b by AFF_1:4;
a,f.a // b,f.b by A2,A5,TRANSGEO:82;
hence contradiction by A1,A4,A6,A7;
end;
theorem
AFP is translational & AFP is Fanoian & f1 is translation & f2 is
translation & g=f1*f1 & g=f2*f2 implies f1=f2
proof
assume that
A1: AFP is translational and
A2: AFP is Fanoian and
A3: f1 is translation and
A4: f2 is translation and
A5: g=f1*f1 & g=f2*f2;
set h=f2"*f1;
A6: f2" is translation by A4,TRANSGEO:85;
h*h=f2"*(f1*(f2"*f1)) by RELAT_1:36
.=f2"*((f1*f2")*f1) by RELAT_1:36
.=f2"*((f2"*f1)*f1) by A1,A3,A6,Th10
.=f2"*(f2"*(f1*f1)) by RELAT_1:36
.=(f2"*f2")*(f1*f1) by RELAT_1:36
.=g"*g by A5,FUNCT_1:44
.=id the carrier of AFP by FUNCT_2:61;
then f2"*f1=id the carrier of AFP by A2,A3,A6,Th13,TRANSGEO:86;
then f2"*f1=f2"*f2 by FUNCT_2:61;
hence thesis by TRANSGEO:5;
end;