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

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 :: thesis: for x being Element of OAS holds f . x = (id the carrier of OAS) . x

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

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

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

( not a,b,x are_collinear implies f . x = x )
by A1, A2, A3, Th50;assume A6:
a,b,x are_collinear
; :: 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 OAS such that

A7: not a,b,z are_collinear by A4, DIRAF:37;

assume A8: x <> a ; :: thesis: f . x = x

A9: not a,z,x are_collinear

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

end;A7: not a,b,z are_collinear by A4, DIRAF:37;

assume A8: x <> a ; :: thesis: f . x = x

A9: not a,z,x are_collinear

proof

f . z = z
by A1, A2, A3, A7, Th50;
assume
a,z,x are_collinear
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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

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