let OAS be OAffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: f = g
A4:
f is dilatation
by A1, Def9;
set b = f . a;
now assume A6:
a <> f . a
;
:: thesis: f = g
for
x being
Element of
OAS holds
f . x = g . x
proof
let x be
Element of
OAS;
:: thesis: f . x = g . x
now assume A7:
LIN a,
f . a,
x
;
:: thesis: f . x = g . xnow assume
x <> a
;
:: thesis: f . x = g . xconsider p being
Element of
OAS such that A8:
not
LIN a,
f . a,
p
by A6, DIRAF:43;
A9:
f . p = g . p
by A1, A2, A3, A8, Th69;
f <> id the
carrier of
OAS
by A6, FUNCT_1:35;
then A10:
(
f . p <> p &
f . x <> x )
by A1, Def9;
not
LIN p,
f . p,
x
proof
assume
LIN p,
f . p,
x
;
:: thesis: contradiction
then
(
LIN p,
f . p,
x &
LIN p,
f . p,
f . x &
LIN p,
f . p,
p )
by A4, Th60, DIRAF:37;
then A11:
LIN x,
f . x,
p
by A10, DIRAF:38;
A12:
LIN a,
f . a,
f . x
by A4, A7, Th60;
LIN a,
f . a,
a
by DIRAF:37;
then A13:
LIN x,
f . x,
a
by A6, A7, A12, DIRAF:38;
LIN a,
f . a,
f . a
by DIRAF:37;
then
LIN x,
f . x,
f . a
by A6, A7, A12, DIRAF:38;
hence
contradiction
by A8, A10, A11, A13, DIRAF:38;
:: thesis: verum
end; hence
f . x = g . x
by A1, A2, A9, Th69;
:: thesis: verum end; hence
f . x = g . x
by A3;
:: thesis: verum end;
hence
f . x = g . x
by A1, A2, A3, Th69;
:: thesis: verum
end; hence
f = g
by FUNCT_2:113;
:: thesis: verum end;
hence
f = g
by A5; :: thesis: verum