let OAS be OAffinSpace; for a being Element of OAS
for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds
f = g
let a be Element of OAS; for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds
f = g
let f, g be Permutation of the carrier of OAS; ( 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, Def9;
A5:
now assume A6:
a <> f . a
;
f = g
for
x being
Element of
OAS holds
f . x = g . x
proof
let x be
Element of
OAS;
f . x = g . x
now assume A7:
LIN a,
f . a,
x
;
f . x = g . xnow A8:
f <> id the
carrier of
OAS
by A6, FUNCT_1:18;
then A9:
f . x <> x
by A1, Def9;
assume
x <> a
;
f . x = g . xconsider p being
Element of
OAS such that A10:
not
LIN a,
f . a,
p
by A6, DIRAF:37;
A11:
f . p <> p
by A1, A8, Def9;
A12:
not
LIN p,
f . p,
x
proof
A13:
LIN a,
f . a,
f . x
by A4, A7, Th60;
LIN a,
f . a,
a
by DIRAF:31;
then A14:
LIN x,
f . x,
a
by A6, A7, A13, DIRAF:32;
A15:
LIN p,
f . p,
p
by DIRAF:31;
LIN a,
f . a,
f . a
by DIRAF:31;
then A16:
LIN x,
f . x,
f . a
by A6, A7, A13, DIRAF:32;
assume A17:
LIN p,
f . p,
x
;
contradiction
then
LIN p,
f . p,
f . x
by A4, Th60;
then
LIN x,
f . x,
p
by A11, A17, A15, DIRAF:32;
hence
contradiction
by A10, A9, A14, A16, DIRAF:32;
verum
end;
f . p = g . p
by A1, A2, A3, A10, Th69;
hence
f . x = g . x
by A1, A2, A12, Th69;
verum end; hence
f . x = g . x
by A3;
verum end;
hence
f . x = g . x
by A1, A2, A3, Th69;
verum
end; hence
f = g
by FUNCT_2:63;
verum end;
hence
f = g
by A5; verum