let AFP be AffinPlane; for a, b, o being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP 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 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let a, b, o be Element of AFP; for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP 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 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let f be Permutation of the carrier of AFP; ( o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP 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 being Element of AFP 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 ) )
assume that
A1:
o <> a
and
A2:
LIN o,a,b
and
A3:
AFP is Desarguesian
; ( ex x, y being Element of AFP st
( ( not f . x = y or ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies ( ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & not f . x = y ) ) or ( f is dilatation & f . o = o & f . a = b ) )
assume A4:
for x, y being Element of AFP 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 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
; ( f is dilatation & f . o = o & f . a = b )
for x, r being Element of AFP holds x,r // f . x,f . r
proof
let x,
r be
Element of
AFP;
x,r // f . x,f . r
set y =
f . x;
set s =
f . r;
A5:
( ( not
LIN o,
a,
r &
LIN o,
r,
f . r &
a,
r // b,
f . r ) or (
LIN o,
a,
r & ex
p,
p9 being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p9 &
a,
p // b,
p9 &
p,
r // p9,
f . r &
LIN o,
a,
f . r ) ) )
by A4;
( ( not
LIN o,
a,
x &
LIN o,
x,
f . x &
a,
x // b,
f . x ) or (
LIN o,
a,
x & ex
p,
p9 being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p9 &
a,
p // b,
p9 &
p,
x // p9,
f . x &
LIN o,
a,
f . x ) ) )
by A4;
hence
x,
r // f . x,
f . r
by A1, A2, A3, A5, Lm1, Lm14, Lm15, Lm16;
verum
end;
hence
f is dilatation
by TRANSGEO:68; ( f . o = o & f . a = b )
thus
f . o = o
f . a = bproof
set y =
f . o;
( ( not
LIN o,
a,
o &
LIN o,
o,
f . o &
a,
o // b,
f . o ) or (
LIN o,
a,
o & ex
p,
p9 being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p9 &
a,
p // b,
p9 &
p,
o // p9,
f . o &
LIN o,
a,
f . o ) ) )
by A4;
hence
f . o = o
by A1, Lm7;
verum
end;
thus
f . a = b
verumproof
set y =
f . a;
LIN o,
a,
a
by AFF_1:7;
then consider p,
p9 being
Element of
AFP 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,
f . a
and A10:
LIN o,
a,
f . a
by A4;
A11:
p,
a // p9,
b
by A8, AFF_1:4;
not
LIN o,
p,
a
by A6, AFF_1:6;
hence
f . a = b
by A2, A7, A9, A10, A11, AFF_1:56;
verum
end;