let AFS be AffinSpace; :: thesis: for x, y being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let x, y be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y )
assume A1:
f is dilatation
; :: thesis: ( not LIN x,f . x,y or LIN x,f . x,f . y )
assume A2:
LIN x,f . x,y
; :: thesis: LIN x,f . x,f . y
now assume A3:
x <> y
;
:: thesis: LIN x,f . x,f . y
(
x,
f . x // x,
y &
x,
y // f . x,
f . y )
by A1, A2, Th85, AFF_1:def 1;
then
x,
f . x // f . x,
f . y
by A3, AFF_1:14;
then
f . x,
x // f . x,
f . y
by AFF_1:13;
then
LIN f . x,
x,
f . y
by AFF_1:def 1;
hence
LIN x,
f . x,
f . y
by AFF_1:15;
:: thesis: verum end;
hence
LIN x,f . x,f . y
by AFF_1:16; :: thesis: verum