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 & b <> f . a & Mid a,b,f . a holds

a,b // f . a,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 & b <> f . a & Mid a,b,f . a holds

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

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

assume that

A1: f is translation and

A2: a <> f . a and

A3: b <> f . a and

A4: Mid a,b,f . a ; :: thesis: a,b // f . a,f . b

A5: a,b // b,f . a by A4, DIRAF:def 3;

A6: f is dilatation by A1;

A7: a,b,f . a are_collinear by A4, DIRAF:28;

then A8: a,f . a,b are_collinear by DIRAF:30;

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

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

a,b // f . a,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 & b <> f . a & Mid a,b,f . a holds

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

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

assume that

A1: f is translation and

A2: a <> f . a and

A3: b <> f . a and

A4: Mid a,b,f . a ; :: thesis: a,b // f . a,f . b

A5: a,b // b,f . a by A4, DIRAF:def 3;

A6: f is dilatation by A1;

A7: a,b,f . a are_collinear by A4, DIRAF:28;

then A8: a,f . a,b are_collinear by DIRAF:30;

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

now :: thesis: ( a <> b implies a,b // f . a,f . b )

hence
a,b // f . a,f . b
by DIRAF:4; :: thesis: verumassume A10:
a <> b
; :: thesis: a,b // f . a,f . b

hence a,b // f . a,f . b by A11, DIRAF:def 4; :: thesis: verum

end;A11: now :: thesis: not a,b // f . b,f . a

a,b '||' f . a,f . b
by A6, Th34;
f . a,a,b are_collinear
by A7, DIRAF:30;

then f . a,a '||' f . a,b by DIRAF:def 5;

then A12: a,f . a '||' b,f . a by DIRAF:22;

consider q being Element of OAS such that

A13: not a,f . a,q are_collinear by A2, DIRAF:37;

consider x being Element of OAS such that

A14: q,b // b,x and

A15: q,a // f . a,x by A5, A10, ANALOAF:def 5;

A16: a,q // x,f . a by A15, DIRAF:2;

A17: Mid q,b,x by A14, DIRAF:def 3;

then A18: x,b,q are_collinear by DIRAF:9, DIRAF:28;

A19: x <> f . a

then a,f . a '||' q,f . q by DIRAF:def 4;

then b,f . a '||' q,f . q by A2, A12, DIRAF:23;

then A25: f . a,b '||' q,f . q by DIRAF:22;

A26: a,f . a,f . b are_collinear by A6, A8, Th47;

( a,q // f . a,f . q & a <> q ) by A1, A13, Lm5, DIRAF:31;

then f . a,f . q // x,f . a by A16, ANALOAF:def 5;

then f . a,f . q '||' f . a,x by DIRAF:def 4;

then f . a,f . q,x are_collinear by DIRAF:def 5;

then A27: x,f . a,f . q are_collinear by DIRAF:30;

A28: b <> f . b by A1, A9;

a,f . a,f . a are_collinear by DIRAF:31;

then A29: b,f . b,f . a are_collinear by A2, A8, A26, DIRAF:32;

a,f . a,a are_collinear by DIRAF:31;

then b,f . b,a are_collinear by A2, A8, A26, DIRAF:32;

then A30: not b,f . b,q are_collinear by A13, A29, A28, DIRAF:32;

A31: not b,f . b,f . q are_collinear

( a,b // a,f . a & a,f . a // b,f . b ) by A1, A8, A5, Lm6, ANALOAF:def 5;

then A34: a,b // b,f . b by A2, DIRAF:3;

assume a,b // f . b,f . a ; :: thesis: contradiction

then b,f . b // f . b,f . a by A10, A34, ANALOAF:def 5;

then Mid b,f . b,f . a by DIRAF:def 3;

then A35: Mid f . a,f . b,b by DIRAF:9;

A36: x,b,b are_collinear by DIRAF:31;

Mid x,b,q by A17, DIRAF:9;

then Mid x,f . a,f . q by A22, A27, A25, PASCH:8;

then consider y being Element of OAS such that

A37: Mid x,y,b and

A38: Mid y,f . b,f . q by A35, A22, PASCH:27;

x,y,b are_collinear by A37, DIRAF:28;

then A39: x,b,y are_collinear by DIRAF:30;

A40: x <> b by A22, DIRAF:31;

then b,q,y are_collinear by A18, A39, A36, DIRAF:32;

then A41: b,q '||' b,y by DIRAF:def 5;

A42: y,f . b,f . q are_collinear by A38, DIRAF:28;

then f . b,f . q,y are_collinear by DIRAF:30;

then A43: f . b,f . q '||' f . b,y by DIRAF:def 5;

b,q '||' f . b,f . q by A6, Th34;

then b,q '||' f . b,y by A33, A43, DIRAF:23;

then f . b,y '||' b,y by A33, A41, DIRAF:23;

then y,b '||' y,f . b by DIRAF:22;

then A44: y,b,f . b are_collinear by DIRAF:def 5;

A45: y,b,b are_collinear by DIRAF:31;

y,b,q are_collinear by A40, A18, A39, A36, DIRAF:32;

hence contradiction by A42, A30, A31, A44, A45, DIRAF:32; :: thesis: verum

end;then f . a,a '||' f . a,b by DIRAF:def 5;

then A12: a,f . a '||' b,f . a by DIRAF:22;

consider q being Element of OAS such that

A13: not a,f . a,q are_collinear by A2, DIRAF:37;

consider x being Element of OAS such that

A14: q,b // b,x and

A15: q,a // f . a,x by A5, A10, ANALOAF:def 5;

A16: a,q // x,f . a by A15, DIRAF:2;

A17: Mid q,b,x by A14, DIRAF:def 3;

then A18: x,b,q are_collinear by DIRAF:9, DIRAF:28;

A19: x <> f . a

proof

A22:
not x,f . a,b are_collinear
assume
x = f . a
; :: thesis: contradiction

then Mid q,b,f . a by A14, DIRAF:def 3;

then q,b,f . a are_collinear by DIRAF:28;

then A20: f . a,b,q are_collinear by DIRAF:30;

A21: a,b,a are_collinear by DIRAF:31;

( f . a,b,a are_collinear & f . a,b,b are_collinear ) by A7, DIRAF:30, DIRAF:31;

then a,b,q are_collinear by A3, A20, DIRAF:32;

hence contradiction by A7, A10, A13, A21, DIRAF:32; :: thesis: verum

end;then Mid q,b,f . a by A14, DIRAF:def 3;

then q,b,f . a are_collinear by DIRAF:28;

then A20: f . a,b,q are_collinear by DIRAF:30;

A21: a,b,a are_collinear by DIRAF:31;

( f . a,b,a are_collinear & f . a,b,b are_collinear ) by A7, DIRAF:30, DIRAF:31;

then a,b,q are_collinear by A3, A20, DIRAF:32;

hence contradiction by A7, A10, A13, A21, DIRAF:32; :: thesis: verum

proof

a,f . a // q,f . q
by A1, A13, Lm5;
assume
x,f . a,b are_collinear
; :: thesis: contradiction

then f . a,x,b are_collinear by DIRAF:30;

then A23: f . a,x '||' f . a,b by DIRAF:def 5;

f . a,b,a are_collinear by A7, DIRAF:30;

then A24: f . a,b '||' f . a,a by DIRAF:def 5;

q,a '||' f . a,x by A15, DIRAF:def 4;

then f . a,b '||' q,a by A19, A23, DIRAF:23;

then f . a,a '||' q,a by A3, A24, DIRAF:23;

then a,f . a '||' a,q by DIRAF:22;

hence contradiction by A13, DIRAF:def 5; :: thesis: verum

end;then f . a,x,b are_collinear by DIRAF:30;

then A23: f . a,x '||' f . a,b by DIRAF:def 5;

f . a,b,a are_collinear by A7, DIRAF:30;

then A24: f . a,b '||' f . a,a by DIRAF:def 5;

q,a '||' f . a,x by A15, DIRAF:def 4;

then f . a,b '||' q,a by A19, A23, DIRAF:23;

then f . a,a '||' q,a by A3, A24, DIRAF:23;

then a,f . a '||' a,q by DIRAF:22;

hence contradiction by A13, DIRAF:def 5; :: thesis: verum

then a,f . a '||' q,f . q by DIRAF:def 4;

then b,f . a '||' q,f . q by A2, A12, DIRAF:23;

then A25: f . a,b '||' q,f . q by DIRAF:22;

A26: a,f . a,f . b are_collinear by A6, A8, Th47;

( a,q // f . a,f . q & a <> q ) by A1, A13, Lm5, DIRAF:31;

then f . a,f . q // x,f . a by A16, ANALOAF:def 5;

then f . a,f . q '||' f . a,x by DIRAF:def 4;

then f . a,f . q,x are_collinear by DIRAF:def 5;

then A27: x,f . a,f . q are_collinear by DIRAF:30;

A28: b <> f . b by A1, A9;

a,f . a,f . a are_collinear by DIRAF:31;

then A29: b,f . b,f . a are_collinear by A2, A8, A26, DIRAF:32;

a,f . a,a are_collinear by DIRAF:31;

then b,f . b,a are_collinear by A2, A8, A26, DIRAF:32;

then A30: not b,f . b,q are_collinear by A13, A29, A28, DIRAF:32;

A31: not b,f . b,f . q are_collinear

proof

then A33:
f . b <> f . q
by DIRAF:31;
b,f . b '||' q,f . q
by A1, Th53;

then A32: b,f . b '||' f . q,q by DIRAF:22;

assume b,f . b,f . q are_collinear ; :: thesis: contradiction

hence contradiction by A28, A30, A32, DIRAF:33; :: thesis: verum

end;then A32: b,f . b '||' f . q,q by DIRAF:22;

assume b,f . b,f . q are_collinear ; :: thesis: contradiction

hence contradiction by A28, A30, A32, DIRAF:33; :: thesis: verum

( a,b // a,f . a & a,f . a // b,f . b ) by A1, A8, A5, Lm6, ANALOAF:def 5;

then A34: a,b // b,f . b by A2, DIRAF:3;

assume a,b // f . b,f . a ; :: thesis: contradiction

then b,f . b // f . b,f . a by A10, A34, ANALOAF:def 5;

then Mid b,f . b,f . a by DIRAF:def 3;

then A35: Mid f . a,f . b,b by DIRAF:9;

A36: x,b,b are_collinear by DIRAF:31;

Mid x,b,q by A17, DIRAF:9;

then Mid x,f . a,f . q by A22, A27, A25, PASCH:8;

then consider y being Element of OAS such that

A37: Mid x,y,b and

A38: Mid y,f . b,f . q by A35, A22, PASCH:27;

x,y,b are_collinear by A37, DIRAF:28;

then A39: x,b,y are_collinear by DIRAF:30;

A40: x <> b by A22, DIRAF:31;

then b,q,y are_collinear by A18, A39, A36, DIRAF:32;

then A41: b,q '||' b,y by DIRAF:def 5;

A42: y,f . b,f . q are_collinear by A38, DIRAF:28;

then f . b,f . q,y are_collinear by DIRAF:30;

then A43: f . b,f . q '||' f . b,y by DIRAF:def 5;

b,q '||' f . b,f . q by A6, Th34;

then b,q '||' f . b,y by A33, A43, DIRAF:23;

then f . b,y '||' b,y by A33, A41, DIRAF:23;

then y,b '||' y,f . b by DIRAF:22;

then A44: y,b,f . b are_collinear by DIRAF:def 5;

A45: y,b,b are_collinear by DIRAF:31;

y,b,q are_collinear by A40, A18, A39, A36, DIRAF:32;

hence contradiction by A42, A30, A31, A44, A45, DIRAF:32; :: thesis: verum

hence a,b // f . a,f . b by A11, DIRAF:def 4; :: thesis: verum