let OAS be OAffinSpace; for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of OAS
let a, b be Element of OAS; for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of OAS
let f be Permutation of the carrier of OAS; ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of OAS )
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 OAS
now for x being Element of OAS holds f . x = (id the carrier of OAS) . xlet x be
Element of
OAS;
f . x = (id the carrier of OAS) . xA5:
now ( a,b,x are_collinear implies f . x = x )assume A6:
a,
b,
x are_collinear
;
f . x = xnow ( x <> a implies f . x = x )consider z being
Element of
OAS such that A7:
not
a,
b,
z are_collinear
by A4, DIRAF:37;
assume A8:
x <> a
;
f . x = xA9:
not
a,
z,
x are_collinear
proof
assume
a,
z,
x are_collinear
;
contradiction
then A10:
a,
x,
z are_collinear
by DIRAF:30;
(
a,
x,
a are_collinear &
a,
x,
b are_collinear )
by A6, DIRAF:30, DIRAF:31;
hence
contradiction
by A8, A7, A10, DIRAF:32;
verum
end;
f . z = z
by A1, A2, A3, A7, Th50;
hence
f . x = x
by A1, A2, A9, Th50;
verum end; hence
f . x = x
by A2;
verum end;
( not
a,
b,
x are_collinear implies
f . x = x )
by A1, A2, A3, Th50;
hence
f . x = (id the carrier of OAS) . x
by A5;
verum end;
hence
f = id the carrier of OAS
by FUNCT_2:63; verum