let OAS be OAffinSpace; for f being Permutation of the carrier of OAS st f is dilatation holds
( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
let f be Permutation of the carrier of OAS; ( f is dilatation implies ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) )
assume A1:
f is dilatation
; ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
A2:
now ( ( for x, y being Element of OAS holds x,f . x '||' y,f . y ) & f <> id the carrier of OAS implies for x being Element of OAS holds not f . x = x )assume A3:
for
x,
y being
Element of
OAS holds
x,
f . x '||' y,
f . y
;
( f <> id the carrier of OAS implies for x being Element of OAS holds not f . x = x )assume
f <> id the
carrier of
OAS
;
for x being Element of OAS holds not f . x = xthen consider y being
Element of
OAS such that A4:
f . y <> (id the carrier of OAS) . y
by FUNCT_2:63;
given x being
Element of
OAS such that A5:
f . x = x
;
contradiction
x <> y
by A5, A4;
then consider z being
Element of
OAS such that A6:
not
x,
y,
z are_collinear
by DIRAF:37;
x,
z '||' f . x,
f . z
by A1, Th34;
then
x,
z,
f . z are_collinear
by A5, DIRAF:def 5;
then A7:
z,
f . z,
x are_collinear
by DIRAF:30;
z,
f . z,
z are_collinear
by DIRAF:31;
then A8:
z,
f . z '||' x,
z
by A7, DIRAF:34;
A9:
f . y <> y
by A4;
x,
y '||' f . x,
f . y
by A1, Th34;
then A10:
x,
y,
f . y are_collinear
by A5, DIRAF:def 5;
then
y,
x,
f . y are_collinear
by DIRAF:30;
then A11:
y,
x '||' y,
f . y
by DIRAF:def 5;
A12:
y,
f . y,
x are_collinear
by A10, DIRAF:30;
A13:
now not z = f . zassume
z = f . z
;
contradictionthen
z,
y '||' z,
f . y
by A1, Th34;
then
z,
y,
f . y are_collinear
by DIRAF:def 5;
then
(
y,
f . y,
y are_collinear &
y,
f . y,
z are_collinear )
by DIRAF:30, DIRAF:31;
hence
contradiction
by A9, A12, A6, DIRAF:32;
verum end;
y,
f . y '||' z,
f . z
by A3;
then
y,
f . y '||' x,
z
by A13, A8, DIRAF:23;
then
y,
x '||' x,
z
by A9, A11, DIRAF:23;
then
x,
y '||' x,
z
by DIRAF:22;
hence
contradiction
by A6, DIRAF:def 5;
verum end;
now ( ( f = id the carrier of OAS or for z being Element of OAS holds f . z <> z ) implies for x, y being Element of OAS holds x,f . x '||' y,f . y )assume A14:
(
f = id the
carrier of
OAS or for
z being
Element of
OAS holds
f . z <> z )
;
for x, y being Element of OAS holds x,f . x '||' y,f . ylet x,
y be
Element of
OAS;
x,f . x '||' y,f . yA15:
x,
y '||' f . x,
f . y
by A1, Th34;
A16:
now ( ( for z being Element of OAS holds f . z <> z ) implies x,f . x '||' y,f . y )assume A17:
for
z being
Element of
OAS holds
f . z <> z
;
x,f . x '||' y,f . yassume A18:
not
x,
f . x '||' y,
f . y
;
contradictionthen consider z being
Element of
OAS such that A19:
x,
f . x,
z are_collinear
and A20:
y,
f . y,
z are_collinear
by A15, Th48;
set t =
f . z;
x,
f . x,
f . z are_collinear
by A1, A19, Th47;
then A21:
x,
f . x '||' z,
f . z
by A19, DIRAF:34;
y,
f . y,
f . z are_collinear
by A1, A20, Th47;
then A22:
y,
f . y '||' z,
f . z
by A20, DIRAF:34;
z <> f . z
by A17;
hence
contradiction
by A18, A21, A22, DIRAF:23;
verum end;
(
f = id the
carrier of
OAS implies
x,
f . x '||' y,
f . y )
by DIRAF:20;
hence
x,
f . x '||' y,
f . y
by A14, A16;
verum end;
hence
( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
by A2; verum