let AFS be AffinSpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( ( 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:
(
f = id the
carrier of
AFS or for
z being
Element of
AFS holds
f . z <> z )
;
:: thesis: for x, y being Element of AFS holds x,f . x // y,f . ylet x,
y be
Element of
AFS;
:: thesis: x,f . x // y,f . yA4:
x,
y // f . x,
f . y
by A1, Th85;
now assume A6:
for
z being
Element of
AFS holds
f . z <> z
;
:: thesis: x,f . x // y,f . yassume A7:
not
x,
f . x // y,
f . y
;
:: thesis: contradictionthen consider z being
Element of
AFS such that A8:
(
LIN x,
f . x,
z &
LIN y,
f . y,
z )
by A4, Th92;
set t =
f . z;
LIN x,
f . x,
f . z
by A1, A8, Th91;
then A9:
x,
f . x // z,
f . z
by A8, AFF_1:19;
(
LIN y,
f . y,
z &
LIN y,
f . y,
f . z &
y <> f . y )
by A1, A6, A8, Th91;
then
y,
f . y // z,
f . z
by AFF_1:19;
then
(
z <> f . z &
z,
f . z // y,
f . y )
by A6, AFF_1:13;
hence
contradiction
by A7, A9, AFF_1:14;
:: thesis: verum end; hence
x,
f . x // y,
f . y
by A3, A5;
:: thesis: verum end;
now assume A10:
for
x,
y being
Element of
AFS holds
x,
f . x // y,
f . y
;
:: thesis: ( f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x )assume A11:
f <> id the
carrier of
AFS
;
:: thesis: for x being Element of AFS holds not f . x = xgiven x being
Element of
AFS such that A12:
f . x = x
;
:: thesis: contradictionconsider y being
Element of
AFS such that A13:
f . y <> (id the carrier of AFS) . y
by A11, FUNCT_2:113;
A14:
f . y <> y
by A13, FUNCT_1:35;
x,
y // f . x,
f . y
by A1, Th85;
then A15:
LIN x,
y,
f . y
by A12, AFF_1:def 1;
then A16:
LIN y,
f . y,
x
by AFF_1:15;
LIN y,
x,
f . y
by A15, AFF_1:15;
then A17:
y,
x // y,
f . y
by AFF_1:def 1;
x <> y
by A12, A13, FUNCT_1:35;
then consider z being
Element of
AFS such that A18:
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 A12, AFF_1:def 1;
then A19:
LIN z,
f . z,
x
by AFF_1:15;
A20:
now assume
z = f . z
;
:: thesis: 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 A14, A16, A18, AFF_1:17;
:: thesis: verum end;
LIN z,
f . z,
z
by AFF_1:16;
then A21:
z,
f . z // x,
z
by A19, AFF_1:19;
y,
f . y // z,
f . z
by A10;
then
y,
f . y // x,
z
by A20, A21, AFF_1:14;
then
y,
x // x,
z
by A14, A17, AFF_1:14;
then
x,
y // x,
z
by AFF_1:13;
hence
contradiction
by A18, AFF_1:def 1;
:: thesis: 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; :: thesis: verum