let AFP be AffinPlane; :: thesis: ( ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) implies AFP is Desarguesian )
assume A1:
for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
; :: thesis: AFP is Desarguesian
now let o,
a,
a',
p,
p',
q,
q' be
Element of
AFP;
:: thesis: ( LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' implies p,q // p',q' )assume that A2:
LIN o,
a,
a'
and A3:
LIN o,
p,
p'
and A4:
LIN o,
q,
q'
and A5:
not
LIN o,
a,
p
and A6:
not
LIN o,
a,
q
and A7:
a,
p // a',
p'
and A8:
a,
q // a',
q'
;
:: thesis: p,q // p',q'A9:
now assume A10:
o <> a'
;
:: thesis: p,q // p',q'
o <> a
by A5, AFF_1:16;
then consider f being
Permutation of the
carrier of
AFP such that A11:
f is
dilatation
and A12:
f . o = o
and A13:
f . a = a'
by A1, A2, A10;
set s =
f . q;
o,
q // o,
f . q
by A11, A12, TRANSGEO:85;
then A14:
LIN o,
q,
f . q
by AFF_1:def 1;
set r =
f . p;
o,
p // o,
f . p
by A11, A12, TRANSGEO:85;
then A15:
LIN o,
p,
f . p
by AFF_1:def 1;
a,
q // a',
f . q
by A11, A13, TRANSGEO:85;
then A16:
f . q = q'
by A2, A4, A6, A8, A14, AFF_1:70;
a,
p // a',
f . p
by A11, A13, TRANSGEO:85;
then
f . p = p'
by A2, A3, A5, A7, A15, AFF_1:70;
hence
p,
q // p',
q'
by A11, A16, TRANSGEO:85;
:: thesis: verum end; now assume A17:
o = a'
;
:: thesis: p,q // p',q'then
o = p'
by A3, A5, A7, AFF_1:69;
then
p' = q'
by A4, A6, A8, A17, AFF_1:69;
hence
p,
q // p',
q'
by AFF_1:12;
:: thesis: verum end; hence
p,
q // p',
q'
by A9;
:: thesis: verum end;
hence
AFP is Desarguesian
by Lm1; :: thesis: verum