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 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:113;
given x being
Element of
AFS such that A5:
f . x = x
;
contradiction
x <> y
by A5, A4, FUNCT_1:35;
then consider z being
Element of
AFS such that A6:
not
LIN x,
y,
z
by AFF_1:22;
x,
z // f . x,
f . z
by A1, Th85;
then
LIN x,
z,
f . z
by A5, AFF_1:def 1;
then A7:
LIN z,
f . z,
x
by AFF_1:15;
LIN z,
f . z,
z
by AFF_1:16;
then A8:
z,
f . z // x,
z
by A7, AFF_1:19;
A9:
f . y <> y
by A4, FUNCT_1:35;
x,
y // f . x,
f . y
by A1, Th85;
then A10:
LIN x,
y,
f . y
by A5, AFF_1:def 1;
then
LIN y,
x,
f . y
by AFF_1:15;
then A11:
y,
x // y,
f . y
by AFF_1:def 1;
A12:
LIN y,
f . y,
x
by A10, AFF_1:15;
A13:
now assume
z = f . z
;
contradictionthen
z,
y // z,
f . y
by A1, Th85;
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:15, AFF_1:16;
hence
contradiction
by A9, A12, A6, AFF_1:17;
verum end;
y,
f . y // z,
f . z
by A3;
then
y,
f . y // x,
z
by A13, A8, AFF_1:14;
then
y,
x // x,
z
by A9, A11, AFF_1:14;
then
x,
y // x,
z
by AFF_1:13;
hence
contradiction
by A6, AFF_1:def 1;
verum end;
now 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, Th85;
A16:
now 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, Th92;
set t =
f . z;
LIN x,
f . x,
f . z
by A1, A19, Th91;
then A21:
x,
f . x // z,
f . z
by A19, AFF_1:19;
LIN y,
f . y,
f . z
by A1, A20, Th91;
then A22:
y,
f . y // z,
f . z
by A20, AFF_1:19;
z <> f . z
by A17;
hence
contradiction
by A18, A21, A22, AFF_1:14;
verum end; 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