let AFS be AffinSpace; :: thesis: for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of AFS
let a, b be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of AFS
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of AFS )
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 AFS
now :: thesis: for x being Element of AFS holds f . x = (id the carrier of AFS) . x
let x be Element of AFS; :: thesis: f . x = (id the carrier of AFS) . x
A5: now :: thesis: ( LIN a,b,x implies f . x = x )
assume A6: LIN a,b,x ; :: thesis: f . x = x
now :: thesis: ( x <> a implies f . x = x )
consider z being Element of AFS such that
A7: not LIN a,b,z by A4, AFF_1:13;
assume A8: x <> a ; :: thesis: f . x = x
A9: not LIN a,z,x
proof
assume LIN a,z,x ; :: thesis: contradiction
then A10: LIN a,x,z by AFF_1:6;
( LIN a,x,a & LIN a,x,b ) by A6, AFF_1:6, AFF_1:7;
hence contradiction by A8, A7, A10, AFF_1:8; :: thesis: verum
end;
f . z = z by A1, A2, A3, A7, Th77;
hence f . x = x by A1, A2, A9, Th77; :: 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, Th77;
hence f . x = (id the carrier of AFS) . x by A5; :: thesis: verum
end;
hence f = id the carrier of AFS by FUNCT_2:63; :: thesis: verum