let AFP be AffinPlane; :: thesis: for a, b being Element of AFP st AFP is translational & a <> b holds
ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )
let a, b be Element of AFP; :: thesis: ( AFP is translational & a <> b implies ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b ) )
defpred S1[ 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 being Element of AFP 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 ; :: thesis: ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )
A3: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A2, Lm6;
A4: for x, y, x9 being Element of AFP st S1[x,y] & S1[x9,y] holds
x = x9
proof
let x, y, x9 be Element of AFP; :: thesis: ( S1[x,y] & S1[x9,y] implies x = 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 being Element of AFP 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 being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x9,y & p,x9 // q,y ) ) ) ; :: thesis: x = x9
A7: now :: thesis: ( LIN a,b,y implies x = x9 )
assume A8: LIN a,b,y ; :: thesis: x = x9
A9: ( LIN a,b,x9 or not a,b // x9,y or not a,x9 // b,y )
proof
assume that
A10: not LIN a,b,x9 and
A11: a,b // x9,y and
a,x9 // b,y ; :: thesis: contradiction
a,b // y,x9 by A11, AFF_1:4;
hence contradiction by A2, A8, A10, AFF_1:9; :: thesis: verum
end;
( LIN a,b,x or not a,b // x,y or not a,x // b,y )
proof
assume that
A12: not LIN a,b,x and
A13: a,b // x,y and
a,x // b,y ; :: thesis: contradiction
a,b // y,x by A13, AFF_1:4;
hence contradiction by A2, A8, A12, AFF_1:9; :: thesis: verum
end;
hence x = x9 by A1, A2, A5, A6, A9, Lm11; :: thesis: verum
end;
now :: thesis: ( not LIN a,b,y implies x = x9 )
assume A14: not LIN a,b,y ; :: thesis: x = x9
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 x = x9 by A16, A15, TRANSGEO:80; :: thesis: verum
end;
hence x = x9 by A7; :: thesis: verum
end;
A17: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A2, Lm7;
A18: for x, y, y9 being Element of AFP st S1[x,y] & S1[x,y9] holds
y = y9 by A1, A2, Lm9, TRANSGEO:80;
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff S1[x,y] ) from TRANSGEO:sch 1(A3, A17, A4, A18);
 then consider f being Permutation of the carrier of AFP such that
A19: for x, y being Element of AFP 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 being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) ) ;
A20: for x being Element of AFP holds a,b // x,f . x
proof
let x be Element of AFP; :: thesis: a,b // x,f . x
set y = f . x;
now :: thesis: ( LIN a,b,x implies a,b // x,f . x )
assume A21: LIN a,b,x ; :: thesis: a,b // x,f . x
then consider p, q being Element of AFP 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,f . x and
p,x // q,f . x by A19;
p <> q by A2, A21, A22, A23, A24, A25, Lm10;
hence a,b // x,f . x by A23, A25, AFF_1:5; :: thesis: verum
end;
hence a,b // x,f . x by A19; :: thesis: verum
end;
for x, y being Element of AFP holds x,y // f . x,f . y
proof
let x, y be Element of AFP; :: thesis: x,y // f . x,f . y
A26: now :: thesis: ( LIN a,b,x & not LIN a,b,y implies x,y // f . x,f . y )
A27: ex x9 being Element of AFP 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 ; :: thesis: x,y // f . x,f . 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 x,y // f . x,f . y by AFF_1:4; :: thesis: verum
end;
A30: now :: thesis: ( not LIN a,b,x & LIN a,b,y implies x,y // f . x,f . y )
A31: ex y9 being Element of AFP 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 ; :: thesis: x,y // f . x,f . y
( a,b // x,f . x & a,x // b,f . x ) by A19, A32;
hence x,y // f . x,f . y by A19, A32, A33, A31; :: thesis: verum
end;
A34: now :: thesis: ( LIN a,b,x & LIN a,b,y implies x,y // f . x,f . y )
assume A35: ( LIN a,b,x & LIN a,b,y ) ; :: thesis: x,y // f . x,f . 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 x,y // f . x,f . y by A2, A36, AFF_1:5; :: thesis: verum
end;
now :: thesis: ( not LIN a,b,x & not LIN a,b,y implies x,y // f . x,f . y )
assume A37: ( not LIN a,b,x & not LIN a,b,y ) ; :: thesis: x,y // f . x,f . 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 x,y // f . x,f . y by A1, A37, A38, Th4; :: thesis: verum
end;
hence x,y // f . x,f . y by A34, A26, A30; :: thesis: verum
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 being Element of AFP such that
A42: not LIN a,b,p by A2, AFF_1:13;
consider q being Element of AFP 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 f . a = b by A19, A42, A43, A41; :: thesis: verum
end;
for x, y being Element of AFP holds x,f . x // y,f . y
proof
let x, y be Element of AFP; :: thesis: x,f . x // y,f . y
( a,b // x,f . x & a,b // y,f . y ) by A20;
hence x,f . x // y,f . y by A2, AFF_1:5; :: thesis: verum
end;
then f is translation by A39, TRANSGEO:82;
hence ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b ) by A40; :: thesis: verum