let OAS be OAffinSpace; :: thesis: for p, q, x being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

let p, q, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x )

assume that

A1: ( f is dilatation & f . p = p ) and

A2: Mid q,p,f . q and

A3: q <> p ; :: thesis: Mid x,p,f . x

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

let p, q, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x )

assume that

A1: ( f is dilatation & f . p = p ) and

A2: Mid q,p,f . q and

A3: q <> p ; :: thesis: Mid x,p,f . x

now :: thesis: ( p,q,x are_collinear implies Mid x,p,f . x )

hence
Mid x,p,f . x
by A1, A2, Th59; :: thesis: verumconsider r being Element of OAS such that

A4: not p,q,r are_collinear by A3, DIRAF:37;

assume A5: p,q,x are_collinear ; :: thesis: Mid x,p,f . x

A6: ( x = p or not p,r,x are_collinear )

hence Mid x,p,f . x by A1, A6, Th59, DIRAF:10; :: thesis: verum

end;A4: not p,q,r are_collinear by A3, DIRAF:37;

assume A5: p,q,x are_collinear ; :: thesis: Mid x,p,f . x

A6: ( x = p or not p,r,x are_collinear )

proof

Mid r,p,f . r
by A1, A2, A4, Th59;
A7:
( p,x,q are_collinear & p,x,p are_collinear )
by A5, DIRAF:30, DIRAF:31;

assume that

A8: x <> p and

A9: p,r,x are_collinear ; :: thesis: contradiction

p,x,r are_collinear by A9, DIRAF:30;

hence contradiction by A4, A8, A7, DIRAF:32; :: thesis: verum

end;assume that

A8: x <> p and

A9: p,r,x are_collinear ; :: thesis: contradiction

p,x,r are_collinear by A9, DIRAF:30;

hence contradiction by A4, A8, A7, DIRAF:32; :: thesis: verum

hence Mid x,p,f . x by A1, A6, Th59, DIRAF:10; :: thesis: verum