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 & b <> f . a & Mid a,b,f . a 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 & b <> f . a & Mid a,b,f . a holds
a,b // f . a,f . b
let f be Permutation of the carrier of OAS; ( 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
; 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 ( a <> b implies a,b // f . a,f . b )assume A10:
a <> b
;
a,b // f . a,f . bA11:
now not a,b // f . b,f . a
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
proof
assume
x = f . a
;
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;
verum
end; A22:
not
x,
f . a,
b are_collinear
proof
assume
x,
f . a,
b are_collinear
;
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;
verum
end;
a,
f . a // q,
f . q
by A1, A13, Lm5;
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
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
;
contradiction
hence
contradiction
by A28, A30, A32, DIRAF:33;
verum
end; then A33:
f . b <> f . q
by DIRAF:31;
(
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
;
contradictionthen
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;
verum end;
a,
b '||' f . a,
f . b
by A6, Th34;
hence
a,
b // f . a,
f . b
by A11, DIRAF:def 4;
verum end;
hence
a,b // f . a,f . b
by DIRAF:4; verum