let OAS be OAffinSpace; 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,b // f . a,f . b
let a, b be 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,b // f . a,f . b
let f be Permutation of the carrier of OAS; ( f is translation & a <> f . a & a,f . a,b are_collinear implies a,b // f . a,f . b )
assume that
A1:
f is translation
and
A2:
a <> f . a
and
A3:
a,f . a,b are_collinear
; a,b // f . a,f . b
f <> id the carrier of OAS
by A2;
then A4:
b <> f . b
by A1;
A5:
f is dilatation
by A1;
now ( a <> b implies a,b // f . a,f . b )assume A6:
a <> b
;
a,b // f . a,f . bA7:
now ( Mid f . a,a,b implies a,b // f . a,f . b )assume A8:
Mid f . a,
a,
b
;
a,b // f . a,f . bA9:
now ( Mid f . b,b,a implies a,b // f . a,f . b )assume
Mid f . b,
b,
a
;
a,b // f . a,f . bthen
Mid a,
b,
f . b
by DIRAF:9;
then
a,
b // b,
f . b
by DIRAF:def 3;
then A10:
a,
b // a,
f . b
by ANALOAF:def 5;
Mid b,
a,
f . a
by A8, DIRAF:9;
then
b,
a // a,
f . a
by DIRAF:def 3;
then A11:
a,
b // f . a,
a
by ANALOAF:def 5;
then
f . a,
a // a,
f . b
by A6, A10, ANALOAF:def 5;
then
f . a,
a // f . a,
f . b
by ANALOAF:def 5;
hence
a,
b // f . a,
f . b
by A10, A11, DIRAF:3;
verum end; A12:
now ( Mid b,a,f . b implies a,b // f . a,f . b )A13:
now ( a = f . b implies a,b // f . a,f . b )assume A14:
a = f . b
;
a,b // f . a,f . b
a,
f . a // b,
f . b
by A1, A2, A3, Lm6;
hence
a,
b // f . a,
f . b
by A14, DIRAF:2;
verum end; assume
Mid b,
a,
f . b
;
a,b // f . a,f . bthen
(
b,
a // f . b,
f . a or
a = f . b )
by A1, A4, Lm8;
hence
a,
b // f . a,
f . b
by A13, DIRAF:2;
verum A15:
now ( Mid b,f . b,a implies a,b // f . a,f . b )assume
Mid b,
f . b,
a
;
a,b // f . a,f . bthen
b,
a // f . b,
f . a
by A1, A4, Lm7;
hence
a,
b // f . a,
f . b
by DIRAF:2;
verum end;
(
a,
f . a,
f . b are_collinear &
a,
f . a,
a are_collinear )
by A3, A5, Th47, DIRAF:31;
hence
a,
b // f . a,
f . b
by A2, A3, A15, A12, A9, DIRAF:29, DIRAF:32;
verum end; A16:
now ( Mid a,b,f . a implies a,b // f . a,f . b )assume A17:
Mid a,
b,
f . a
;
a,b // f . a,f . b
(
b = f . a implies
a,
b // f . a,
f . b )
by A1, A2, A3, Lm6;
hence
a,
b // f . a,
f . b
by A1, A2, A17, Lm8;
verum end;
(
Mid a,
f . a,
b implies
a,
b // f . a,
f . b )
by A1, A2, Lm7;
hence
a,
b // f . a,
f . b
by A3, A7, A16, DIRAF:29;
verum end;
hence
a,b // f . a,f . b
by DIRAF:4; verum