let AFS be AffinSpace; for f being Permutation of the carrier of AFS st f is dilatation holds
( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )
let f be Permutation of the carrier of AFS; ( f is dilatation implies ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) )
assume A1:
f is dilatation
; ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )
A2:
now ( ( for x, y being Element of AFS holds x,f . x // y,f . y ) & f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x )assume A3:
for
x,
y being
Element of
AFS holds
x,
f . x // y,
f . y
;
( f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x )assume
f <> id the
carrier of
AFS
;
for x being Element of AFS holds not f . x = xthen consider y being
Element of
AFS such that A4:
f . y <> (id the carrier of AFS) . y
by FUNCT_2:63;
given x being
Element of
AFS such that A5:
f . x = x
;
contradiction
x <> y
by A5, A4;
then consider z being
Element of
AFS such that A6:
not
LIN x,
y,
z
by AFF_1:13;
x,
z // f . x,
f . z
by A1, Th68;
then
LIN x,
z,
f . z
by A5, AFF_1:def 1;
then A7:
LIN z,
f . z,
x
by AFF_1:6;
LIN z,
f . z,
z
by AFF_1:7;
then A8:
z,
f . z // x,
z
by A7, AFF_1:10;
A9:
f . y <> y
by A4;
x,
y // f . x,
f . y
by A1, Th68;
then A10:
LIN x,
y,
f . y
by A5, AFF_1:def 1;
then
LIN y,
x,
f . y
by AFF_1:6;
then A11:
y,
x // y,
f . y
by AFF_1:def 1;
A12:
LIN y,
f . y,
x
by A10, AFF_1:6;
A13:
now not z = f . zassume
z = f . z
;
contradictionthen
z,
y // z,
f . y
by A1, Th68;
then
LIN z,
y,
f . y
by AFF_1:def 1;
then
(
LIN y,
f . y,
y &
LIN y,
f . y,
z )
by AFF_1:6, AFF_1:7;
hence
contradiction
by A9, A12, A6, AFF_1:8;
verum end;
y,
f . y // z,
f . z
by A3;
then
y,
f . y // x,
z
by A13, A8, AFF_1:5;
then
y,
x // x,
z
by A9, A11, AFF_1:5;
then
x,
y // x,
z
by AFF_1:4;
hence
contradiction
by A6, AFF_1:def 1;
verum end;
now ( ( f = id the carrier of AFS or for z being Element of AFS holds f . z <> z ) implies for x, y being Element of AFS holds x,f . x // y,f . y )assume A14:
(
f = id the
carrier of
AFS or for
z being
Element of
AFS holds
f . z <> z )
;
for x, y being Element of AFS holds x,f . x // y,f . ylet x,
y be
Element of
AFS;
x,f . x // y,f . yA15:
x,
y // f . x,
f . y
by A1, Th68;
A16:
now ( ( for z being Element of AFS holds f . z <> z ) implies x,f . x // y,f . y )assume A17:
for
z being
Element of
AFS holds
f . z <> z
;
x,f . x // y,f . yassume A18:
not
x,
f . x // y,
f . y
;
contradictionthen consider z being
Element of
AFS such that A19:
LIN x,
f . x,
z
and A20:
LIN y,
f . y,
z
by A15, Th75;
set t =
f . z;
LIN x,
f . x,
f . z
by A1, A19, Th74;
then A21:
x,
f . x // z,
f . z
by A19, AFF_1:10;
LIN y,
f . y,
f . z
by A1, A20, Th74;
then A22:
y,
f . y // z,
f . z
by A20, AFF_1:10;
z <> f . z
by A17;
hence
contradiction
by A18, A21, A22, AFF_1:5;
verum end;
(
f = id the
carrier of
AFS implies
x,
f . x // y,
f . y )
by AFF_1:3;
hence
x,
f . x // y,
f . y
by A14, A16;
verum end;
hence
( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )
by A2; verum