let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS

for f being Permutation of the carrier of OAS st f is translation & a <> f . a & a,f . a,b are_collinear holds

a,f . a // b,f . b

let a, b be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & a,f . a,b are_collinear holds

a,f . a // b,f . b

let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & a,f . a,b are_collinear implies a,f . a // b,f . b )

assume that

A1: f is translation and

A2: a <> f . a and

A3: a,f . a,b are_collinear ; :: thesis: a,f . a // b,f . b

consider p being Element of OAS such that

A4: not a,f . a,p are_collinear by A2, DIRAF:37;

A5: f is dilatation by A1;

A6: f <> id the carrier of OAS by A2;

then A7: p <> f . p by A1;

A8: b <> f . b by A1, A6;

not p,f . p,b are_collinear

not p,f . p,a are_collinear

hence a,f . a // b,f . b by A7, A13, ANALOAF:def 5; :: thesis: verum

for f being Permutation of the carrier of OAS st f is translation & a <> f . a & a,f . a,b are_collinear holds

a,f . a // b,f . b

let a, b be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & a,f . a,b are_collinear holds

a,f . a // b,f . b

let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & a,f . a,b are_collinear implies a,f . a // b,f . b )

assume that

A1: f is translation and

A2: a <> f . a and

A3: a,f . a,b are_collinear ; :: thesis: a,f . a // b,f . b

consider p being Element of OAS such that

A4: not a,f . a,p are_collinear by A2, DIRAF:37;

A5: f is dilatation by A1;

A6: f <> id the carrier of OAS by A2;

then A7: p <> f . p by A1;

A8: b <> f . b by A1, A6;

not p,f . p,b are_collinear

proof

then A13:
p,f . p // b,f . b
by A1, Lm5;
A9:
p,f . p,p are_collinear
by DIRAF:31;

assume A10: p,f . p,b are_collinear ; :: thesis: contradiction

then p,f . p,f . b are_collinear by A5, Th47;

then A11: b,f . b,p are_collinear by A7, A10, A9, DIRAF:32;

( a,f . a,f . b are_collinear & a,f . a,a are_collinear ) by A3, A5, Th47, DIRAF:31;

then A12: b,f . b,a are_collinear by A2, A3, DIRAF:32;

then b,f . b,f . a are_collinear by A5, Th47;

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

end;assume A10: p,f . p,b are_collinear ; :: thesis: contradiction

then p,f . p,f . b are_collinear by A5, Th47;

then A11: b,f . b,p are_collinear by A7, A10, A9, DIRAF:32;

( a,f . a,f . b are_collinear & a,f . a,a are_collinear ) by A3, A5, Th47, DIRAF:31;

then A12: b,f . b,a are_collinear by A2, A3, DIRAF:32;

then b,f . b,f . a are_collinear by A5, Th47;

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

not p,f . p,a are_collinear

proof

then
p,f . p // a,f . a
by A1, Lm5;
assume A14:
p,f . p,a are_collinear
; :: thesis: contradiction

then ( p,f . p,p are_collinear & p,f . p,f . a are_collinear ) by A5, Th47, DIRAF:31;

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

end;then ( p,f . p,p are_collinear & p,f . p,f . a are_collinear ) by A5, Th47, DIRAF:31;

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

hence a,f . a // b,f . b by A7, A13, ANALOAF:def 5; :: thesis: verum