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 A1:
( AFP is translational & a <> b )
; :: thesis: ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )
then A2:
for x being Element of AFP ex y being Element of AFP st S1[x,y]
by Lm6;
A3:
for y being Element of AFP ex x being Element of AFP st S1[x,y]
by A1, Lm7;
A4:
for x, y, y' being Element of AFP st S1[x,y] & S1[x,y'] holds
y = y'
by A1, Lm9, TRANSGEO:97;
A5:
for x, y, x' being Element of AFP st S1[x,y] & S1[x',y] holds
x = x'
proof
let x,
y,
x' be
Element of
AFP;
:: thesis: ( S1[x,y] & S1[x',y] implies x = x' )
assume A6:
( ( ( 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 ) ) ) & ( ( 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 ) ) ) )
;
:: thesis: x = x'
A7:
now assume A8:
not
LIN a,
b,
y
;
:: thesis: x = x'then A9:
not
LIN b,
a,
y
by A1, A6, Lm5, Lm10;
A10:
(
b,
a // y,
x &
b,
y // a,
x )
by A1, A6, A8, Lm10, AFF_1:13;
(
b,
a // y,
x' &
b,
y // a,
x' )
by A1, A6, A8, Lm10, AFF_1:13;
hence
x = x'
by A9, A10, TRANSGEO:97;
:: thesis: verum end;
now assume A11:
LIN a,
b,
y
;
:: thesis: x = x'A12:
(
LIN a,
b,
x or not
a,
b // x,
y or not
a,
x // b,
y )
proof
assume A13:
( not
LIN a,
b,
x &
a,
b // x,
y &
a,
x // b,
y )
;
:: thesis: contradiction
then
a,
b // y,
x
by AFF_1:13;
hence
contradiction
by A1, A11, A13, AFF_1:18;
:: thesis: verum
end;
(
LIN a,
b,
x' or not
a,
b // x',
y or not
a,
x' // b,
y )
proof
assume A14:
( not
LIN a,
b,
x' &
a,
b // x',
y &
a,
x' // b,
y )
;
:: thesis: contradiction
then
a,
b // y,
x'
by AFF_1:13;
hence
contradiction
by A1, A11, A14, AFF_1:18;
:: thesis: verum
end; hence
x = x'
by A1, A6, A12, Lm11;
:: thesis: verum end;
hence
x = x'
by A7;
:: thesis: verum
end;
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(A2, A3, A5, A4);
then consider f being Permutation of the carrier of AFP such that
A15:
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 ) ) ) )
;
A16:
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 assume A17:
LIN a,
b,
x
;
:: thesis: a,b // x,f . xthen consider p,
q being
Element of
AFP such that A18:
( not
LIN a,
b,
p &
a,
b // p,
q &
a,
p // b,
q &
p,
q // x,
f . x &
p,
x // q,
f . x )
by A15;
p <> q
by A1, A17, A18, Lm10;
hence
a,
b // x,
f . x
by A18, AFF_1:14;
:: thesis: verum end;
hence
a,
b // x,
f . x
by A15;
:: thesis: verum
end;
A19:
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 A16;
hence
x,
f . x // y,
f . y
by A1, AFF_1:14;
:: 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
A20:
now assume A21:
( not
LIN a,
b,
x & not
LIN a,
b,
y )
;
:: thesis: x,y // f . x,f . ythen
(
a,
x // b,
f . x &
a,
y // b,
f . y &
a,
b // x,
f . x &
a,
b // y,
f . y )
by A15;
hence
x,
y // f . x,
f . y
by A1, A21, Th6;
:: thesis: verum end;
A22:
now assume A23:
(
LIN a,
b,
x &
LIN a,
b,
y )
;
:: thesis: x,y // f . x,f . ythen A24:
a,
b // x,
y
by AFF_1:19;
(
LIN a,
b,
f . x &
LIN a,
b,
f . y )
by A1, A16, A23, AFF_1:18;
then
a,
b // f . x,
f . y
by AFF_1:19;
hence
x,
y // f . x,
f . y
by A1, A24, AFF_1:14;
:: thesis: verum end;
A25:
now assume A26:
(
LIN a,
b,
x & not
LIN a,
b,
y )
;
:: thesis: x,y // f . x,f . ythen A27:
(
a,
b // y,
f . y &
a,
y // b,
f . y )
by A15;
ex
x' being
Element of
AFP st
(
y,
f . y // x,
x' &
y,
x // f . y,
x' )
by DIRAF:47;
then
y,
x // f . y,
f . x
by A15, A26, A27;
hence
x,
y // f . x,
f . y
by AFF_1:13;
:: thesis: verum end;
now assume A28:
( not
LIN a,
b,
x &
LIN a,
b,
y )
;
:: thesis: x,y // f . x,f . ythen A29:
(
a,
b // x,
f . x &
a,
x // b,
f . x )
by A15;
ex
y' being
Element of
AFP st
(
x,
f . x // y,
y' &
x,
y // f . x,
y' )
by DIRAF:47;
hence
x,
y // f . x,
f . y
by A15, A28, A29;
:: thesis: verum end;
hence
x,
y // f . x,
f . y
by A20, A22, A25;
:: thesis: verum
end;
then
f is dilatation
by TRANSGEO:85;
then A30:
f is translation
by A19, TRANSGEO:100;
f . a = b
proof
consider p being
Element of
AFP such that A31:
not
LIN a,
b,
p
by A1, AFF_1:22;
consider q being
Element of
AFP such that A32:
(
a,
b // p,
q &
a,
p // b,
q )
by DIRAF:47;
A33:
(
p,
q // a,
b &
p,
a // q,
b )
by A32, AFF_1:13;
(
p,
q // a,
b &
LIN a,
b,
a )
by A32, AFF_1:13, AFF_1:16;
hence
f . a = b
by A15, A31, A32, A33;
:: thesis: verum
end;
hence
ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )
by A30; :: thesis: verum