let OAS be OAffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: f = id the carrier of OAS
now let x be
Element of
OAS;
:: thesis: f . x = (id the carrier of OAS) . xA5:
now assume A6:
LIN a,
b,
x
;
:: thesis: f . x = xnow consider z being
Element of
OAS such that A7:
not
LIN a,
b,
z
by A4, DIRAF:43;
assume A8:
x <> a
;
:: thesis: f . x = xA9:
not
LIN a,
z,
x
proof
assume
LIN a,
z,
x
;
:: thesis: contradiction
then A10:
LIN a,
x,
z
by DIRAF:36;
(
LIN a,
x,
a &
LIN a,
x,
b )
by A6, DIRAF:36, DIRAF:37;
hence
contradiction
by A8, A7, A10, DIRAF:38;
:: thesis: verum
end;
f . z = z
by A1, A2, A3, A7, Th63;
hence
f . x = x
by A1, A2, A9, Th63;
:: thesis: verum end; hence
f . x = x
by A2;
:: thesis: verum end;
( not
LIN a,
b,
x implies
f . x = x )
by A1, A2, A3, Th63;
hence
f . x = (id the carrier of OAS) . x
by A5, FUNCT_1:35;
:: thesis: verum end;
hence
f = id the carrier of OAS
by FUNCT_2:113; :: thesis: verum