let AFS be AffinSpace; for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of AFS
let a, b be Element of AFS; for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of AFS
let f be Permutation of the carrier of AFS; ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of AFS )
assume that
A1:
f is dilatation
and
A2:
f . a = a
and
A3:
f . b = b
and
A4:
a <> b
; f = id the carrier of AFS
now for x being Element of AFS holds f . x = (id the carrier of AFS) . xlet x be
Element of
AFS;
f . x = (id the carrier of AFS) . xA5:
now ( LIN a,b,x implies f . x = x )assume A6:
LIN a,
b,
x
;
f . x = xnow ( x <> a implies f . x = x )consider z being
Element of
AFS such that A7:
not
LIN a,
b,
z
by A4, AFF_1:13;
assume A8:
x <> a
;
f . x = xA9:
not
LIN a,
z,
x
proof
assume
LIN a,
z,
x
;
contradiction
then A10:
LIN a,
x,
z
by AFF_1:6;
(
LIN a,
x,
a &
LIN a,
x,
b )
by A6, AFF_1:6, AFF_1:7;
hence
contradiction
by A8, A7, A10, AFF_1:8;
verum
end;
f . z = z
by A1, A2, A3, A7, Th77;
hence
f . x = x
by A1, A2, A9, Th77;
verum end; hence
f . x = x
by A2;
verum end;
( not
LIN a,
b,
x implies
f . x = x )
by A1, A2, A3, Th77;
hence
f . x = (id the carrier of AFS) . x
by A5;
verum end;
hence
f = id the carrier of AFS
by FUNCT_2:63; verum