let AFP be AffinPlane; :: thesis: for o, a, b being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & o <> b & 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let o, a, b be Element of AFP; :: thesis: for f being Permutation of the carrier of AFP st o <> a & o <> b & 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let f be Permutation of the carrier of AFP; :: thesis: ( o <> a & o <> b & 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) ) implies ( f is dilatation & f . o = o & f . a = b ) )
assume that
A1:
( o <> a & o <> b & LIN o,a,b )
and
A2:
AFP is Desarguesian
; :: thesis: ( 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) & not f . x = y ) ) or ( f is dilatation & f . o = o & f . a = b ) )
assume A3:
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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) )
; :: thesis: ( 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;
:: thesis: x,r // f . x,f . r
set y =
f . x;
set s =
f . r;
A4:
( ( not
LIN o,
a,
x &
LIN o,
x,
f . x &
a,
x // b,
f . x ) or (
LIN o,
a,
x & ex
p,
p' being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p' &
a,
p // b,
p' &
p,
x // p',
f . x &
LIN o,
a,
f . x ) ) )
by A3;
( ( not
LIN o,
a,
r &
LIN o,
r,
f . r &
a,
r // b,
f . r ) or (
LIN o,
a,
r & ex
p,
p' being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p' &
a,
p // b,
p' &
p,
r // p',
f . r &
LIN o,
a,
f . r ) ) )
by A3;
hence
x,
r // f . x,
f . r
by A1, A2, A4, Lm1, Lm14, Lm15, Lm16;
:: thesis: verum
end;
hence
f is dilatation
by TRANSGEO:85; :: thesis: ( f . o = o & f . a = b )
thus
f . o = o
:: thesis: 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,
p' being
Element of
AFP st
( not
LIN o,
a,
p &
LIN o,
p,
p' &
a,
p // b,
p' &
p,
o // p',
f . o &
LIN o,
a,
f . o ) ) )
by A3;
hence
f . o = o
by A1, Lm7;
:: thesis: verum
end;
thus
f . a = b
:: thesis: verumproof
set y =
f . a;
LIN o,
a,
a
by AFF_1:16;
then consider p,
p' being
Element of
AFP such that A5:
( not
LIN o,
a,
p &
LIN o,
p,
p' &
a,
p // b,
p' &
p,
a // p',
f . a &
LIN o,
a,
f . a )
by A3;
A6:
not
LIN o,
p,
a
by A5, AFF_1:15;
p,
a // p',
b
by A5, AFF_1:13;
hence
f . a = b
by A1, A5, A6, AFF_1:70;
:: thesis: verum
end;