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

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

hence
f = id the carrier of AFS
by FUNCT_2:63; :: thesis: verumlet x be Element of AFS; :: thesis: f . x = (id the carrier of AFS) . x

hence f . x = (id the carrier of AFS) . x by A5; :: thesis: verum

end;A5: now :: thesis: ( LIN a,b,x implies f . x = x )

( not LIN a,b,x implies f . x = x )
by A1, A2, A3, Th77;assume A6:
LIN a,b,x
; :: thesis: f . x = x

end;now :: thesis: ( x <> a implies f . x = x )

hence
f . x = x
by A2; :: thesis: verumconsider 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

hence f . x = x by A1, A2, A9, Th77; :: thesis: verum

end;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

f . z = z
by A1, A2, A3, A7, Th77;
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;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

hence f . x = x by A1, A2, A9, Th77; :: thesis: verum

hence f . x = (id the carrier of AFS) . x by A5; :: thesis: verum