let AFS be AffinSpace; for a being Element of AFS
for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds
f = g
let a be Element of AFS; for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds
f = g
let f, g be Permutation of the carrier of AFS; ( f is translation & g is translation & f . a = g . a implies f = g )
assume that
A1:
f is translation
and
A2:
g is translation
and
A3:
f . a = g . a
; f = g
set b = f . a;
A4:
f is dilatation
by A1;
A5:
now ( a <> f . a implies f = g )assume A6:
a <> f . a
;
f = g
for
x being
Element of
AFS holds
f . x = g . x
proof
let x be
Element of
AFS;
f . x = g . x
now ( LIN a,f . a,x implies f . x = g . x )assume A7:
LIN a,
f . a,
x
;
f . x = g . xnow ( x <> a implies f . x = g . x )A8:
f <> id the
carrier of
AFS
by A6;
then A9:
f . x <> x
by A1;
assume
x <> a
;
f . x = g . xconsider p being
Element of
AFS such that A10:
not
LIN a,
f . a,
p
by A6, AFF_1:13;
A11:
f . p <> p
by A1, A8;
A12:
not
LIN p,
f . p,
x
proof
A13:
LIN a,
f . a,
f . x
by A4, A7, Th74;
LIN a,
f . a,
a
by AFF_1:7;
then A14:
LIN x,
f . x,
a
by A6, A7, A13, AFF_1:8;
A15:
LIN p,
f . p,
p
by AFF_1:7;
LIN a,
f . a,
f . a
by AFF_1:7;
then A16:
LIN x,
f . x,
f . a
by A6, A7, A13, AFF_1:8;
assume A17:
LIN p,
f . p,
x
;
contradiction
then
LIN p,
f . p,
f . x
by A4, Th74;
then
LIN x,
f . x,
p
by A11, A17, A15, AFF_1:8;
hence
contradiction
by A10, A9, A14, A16, AFF_1:8;
verum
end;
f . p = g . p
by A1, A2, A3, A10, Th83;
hence
f . x = g . x
by A1, A2, A12, Th83;
verum end; hence
f . x = g . x
by A3;
verum end;
hence
f . x = g . x
by A1, A2, A3, Th83;
verum
end; hence
f = g
by FUNCT_2:63;
verum end;
( f . a = a implies f = g )
by A1, A2, A3;
hence
f = g
by A5; verum