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;
A5:
now ( a <> f . a implies f = g )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 ( a,f . a,x are_collinear implies f . x = g . x )assume A7:
a,
f . a,
x are_collinear
;
f . x = g . xnow ( x <> a implies f . x = g . x )A8:
f <> id the
carrier of
OAS
by A6;
then A9:
f . x <> x
by A1;
assume
x <> a
;
f . x = g . xconsider p being
Element of
OAS such that A10:
not
a,
f . a,
p are_collinear
by A6, DIRAF:37;
A11:
f . p <> p
by A1, A8;
A12:
not
p,
f . p,
x are_collinear
proof
A13:
a,
f . a,
f . x are_collinear
by A4, A7, Th47;
a,
f . a,
a are_collinear
by DIRAF:31;
then A14:
x,
f . x,
a are_collinear
by A6, A7, A13, DIRAF:32;
A15:
p,
f . p,
p are_collinear
by DIRAF:31;
a,
f . a,
f . a are_collinear
by DIRAF:31;
then A16:
x,
f . x,
f . a are_collinear
by A6, A7, A13, DIRAF:32;
assume A17:
p,
f . p,
x are_collinear
;
contradiction
then
p,
f . p,
f . x are_collinear
by A4, Th47;
then
x,
f . x,
p are_collinear
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, Th54;
hence
f . x = g . x
by A1, A2, A12, Th54;
verum end; hence
f . x = g . x
by A3;
verum end;
hence
f . x = g . x
by A1, A2, A3, Th54;
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