let OAS be OAffinSpace; for a, b, c, d, p being Element of OAS st Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p <> c holds
Mid p,d,a
let a, b, c, d, p be Element of OAS; ( Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p <> c implies Mid p,d,a )
assume that
A1:
Mid p,c,b
and
A2:
c,d // b,a
and
A3:
p,d // p,a
and
A4:
not p,a,b are_collinear
and
A5:
p <> c
; Mid p,d,a
A6:
p,c,b are_collinear
by A1, DIRAF:28;
now ( Mid p,a,d implies Mid p,d,a )assume A7:
Mid p,
a,
d
;
Mid p,d,aA8:
now ( b <> c & d <> a implies Mid p,d,a )A9:
p <> a
by A4, DIRAF:31;
assume that A10:
b <> c
and A11:
d <> a
;
Mid p,d,aassume
not
Mid p,
d,
a
;
contradictionthen
Mid p,
a,
d
by A3, DIRAF:7;
then
p,
a // a,
d
by DIRAF:def 3;
then consider e1 being
Element of
OAS such that A12:
c,
a // a,
e1
and A13:
c,
p // d,
e1
by A9, ANALOAF:def 5;
A14:
d,
e1 // c,
p
by A13, DIRAF:2;
A15:
c <> e1
by A12, DIRAF:def 3, A4, A6, DIRAF:8;
Mid b,
c,
p
by A1, DIRAF:9;
then A16:
b,
c // c,
p
by DIRAF:def 3;
then A17:
c,
p // b,
c
by DIRAF:2;
consider e2 being
Element of
OAS such that A18:
b,
a // a,
e2
and A19:
b,
c // e1,
e2
by A4, A6, A12, ANALOAF:def 5;
consider e3 being
Element of
OAS such that A20:
b,
c // e2,
e3
and A21:
b,
e2 // c,
e3
and
c <> e3
by ANALOAF:def 5;
A22:
a <> b
by A4, DIRAF:31;
A23:
Mid c,
a,
e1
by A12, DIRAF:def 3;
A24:
d <> e1
proof
(
Mid p,
d,
a or
Mid p,
a,
d )
by A3, DIRAF:7;
then
(
p,
d,
a are_collinear or
p,
a,
d are_collinear )
by DIRAF:28;
then A25:
d,
a,
p are_collinear
by DIRAF:30;
A26:
d,
a,
a are_collinear
by DIRAF:31;
assume
d = e1
;
contradiction
then
c,
a,
d are_collinear
by A23, DIRAF:28;
then
d,
a,
c are_collinear
by DIRAF:30;
then
d,
a,
b are_collinear
by A5, A6, A25, DIRAF:35;
hence
contradiction
by A4, A11, A25, A26, DIRAF:32;
verum
end;
b,
a // b,
e2
by A18, ANALOAF:def 5;
then A27:
c,
d // b,
e2
by A2, A22, DIRAF:3;
b <> e2
by A22, A18, ANALOAF:def 5;
then
c,
d // c,
e3
by A21, A27, DIRAF:3;
then
(
Mid c,
d,
e3 or
Mid c,
e3,
d )
by DIRAF:7;
then
(
c,
d,
e3 are_collinear or
c,
e3,
d are_collinear )
by DIRAF:28;
then A28:
d,
e3,
c are_collinear
by DIRAF:30;
e1,
e2 // c,
p
by A10, A19, A16, ANALOAF:def 5;
then A29:
e1,
e2 // d,
e1
by A5, A13, DIRAF:3;
then
d,
e1 // e1,
e2
by DIRAF:2;
then A30:
d,
e1 // d,
e2
by ANALOAF:def 5;
then
d,
e2 // d,
e1
by DIRAF:2;
then
d,
e2 // c,
p
by A24, A14, DIRAF:3;
then
d,
e2 // b,
c
by A5, A17, DIRAF:3;
then A31:
d,
e2 // e2,
e3
by A10, A20, DIRAF:3;
then
Mid d,
e2,
e3
by DIRAF:def 3;
then
d,
e2,
e3 are_collinear
by DIRAF:28;
then A32:
d,
e3,
e2 are_collinear
by DIRAF:30;
A33:
d <> e2
by A24, A29, ANALOAF:def 5;
then A34:
d <> e3
by A31, ANALOAF:def 5;
d,
e2 // d,
e3
by A31, ANALOAF:def 5;
then
d,
e1 // d,
e3
by A30, A33, DIRAF:3;
then
(
Mid d,
e1,
e3 or
Mid d,
e3,
e1 )
by DIRAF:7;
then
(
d,
e1,
e3 are_collinear or
d,
e3,
e1 are_collinear )
by DIRAF:28;
then A35:
d,
e3,
e1 are_collinear
by DIRAF:30;
c,
a,
e1 are_collinear
by A23, DIRAF:28;
then
c,
e1,
a are_collinear
by DIRAF:30;
then A36:
d,
e3,
a are_collinear
by A15, A28, A35, DIRAF:35;
A37:
a <> e1
proof
p,
a // a,
d
by A7, DIRAF:def 3;
then A38:
d,
a // a,
p
by DIRAF:2;
assume
a = e1
;
contradiction
then
c,
p // a,
p
by A11, A13, A38, DIRAF:3;
then
p,
c // p,
a
by DIRAF:2;
then
(
Mid p,
c,
a or
Mid p,
a,
c )
by DIRAF:7;
then
(
p,
c,
a are_collinear or
p,
a,
c are_collinear )
by DIRAF:28;
then A39:
p,
c,
a are_collinear
by DIRAF:30;
p,
c,
p are_collinear
by DIRAF:31;
hence
contradiction
by A4, A5, A6, A39, DIRAF:32;
verum
end; A40:
a <> e2
proof
assume A41:
a = e2
;
contradiction
e1,
a // a,
c
by A12, DIRAF:2;
then
b,
c // a,
c
by A19, A37, A41, DIRAF:3;
then
c,
b // c,
a
by DIRAF:2;
then
(
Mid c,
b,
a or
Mid c,
a,
b )
by DIRAF:7;
then
(
c,
b,
a are_collinear or
c,
a,
b are_collinear )
by DIRAF:28;
then A42:
c,
b,
a are_collinear
by DIRAF:30;
A43:
c,
b,
b are_collinear
by DIRAF:31;
c,
b,
p are_collinear
by A6, DIRAF:30;
hence
contradiction
by A4, A10, A42, A43, DIRAF:32;
verum
end;
Mid b,
a,
e2
by A18, DIRAF:def 3;
then
b,
a,
e2 are_collinear
by DIRAF:28;
then
a,
e2,
b are_collinear
by DIRAF:30;
then A44:
d,
e3,
b are_collinear
by A40, A36, A32, DIRAF:35;
c,
b,
p are_collinear
by A6, DIRAF:30;
then
d,
e3,
p are_collinear
by A10, A28, A44, DIRAF:35;
hence
contradiction
by A4, A34, A36, A44, DIRAF:32;
verum end; A45:
p,
a,
d are_collinear
by A7, DIRAF:28;
now ( b = c implies a = d )assume
b = c
;
a = dthen
(
Mid b,
d,
a or
Mid b,
a,
d )
by A2, DIRAF:7;
then
(
b,
d,
a are_collinear or
b,
a,
d are_collinear )
by DIRAF:28;
then A46:
d,
a,
b are_collinear
by DIRAF:30;
A47:
d,
a,
a are_collinear
by DIRAF:31;
d,
a,
p are_collinear
by A45, DIRAF:30;
hence
a = d
by A4, A46, A47, DIRAF:32;
verum end; hence
Mid p,
d,
a
by A8, DIRAF:10;
verum end;
hence
Mid p,d,a
by A3, DIRAF:7; verum