let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace (TOP-REAL 3)); ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear & not p1,q1,r1 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1:
( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear )
and
A2:
not p1,q1,r1 are_collinear
; r1,r2,r3 are_collinear
consider pp1 being Element of (TOP-REAL 3) such that
A3:
( not pp1 is zero & Dir pp1 = p1 )
by ANPROJ_1:26;
consider pp2 being Element of (TOP-REAL 3) such that
A4:
( not pp2 is zero & Dir pp2 = p2 )
by ANPROJ_1:26;
consider pp3 being Element of (TOP-REAL 3) such that
A5:
( not pp3 is zero & Dir pp3 = p3 )
by ANPROJ_1:26;
consider pp4 being Element of (TOP-REAL 3) such that
A6:
( not pp4 is zero & Dir pp4 = q1 )
by ANPROJ_1:26;
consider pp5 being Element of (TOP-REAL 3) such that
A7:
( not pp5 is zero & Dir pp5 = q2 )
by ANPROJ_1:26;
consider pp6 being Element of (TOP-REAL 3) such that
A8:
( not pp6 is zero & Dir pp6 = q3 )
by ANPROJ_1:26;
consider pp7 being Element of (TOP-REAL 3) such that
A9:
( not pp7 is zero & Dir pp7 = r1 )
by ANPROJ_1:26;
consider pp8 being Element of (TOP-REAL 3) such that
A10:
( not pp8 is zero & Dir pp8 = r2 )
by ANPROJ_1:26;
consider pp9 being Element of (TOP-REAL 3) such that
A11:
( not pp9 is zero & Dir pp9 = r3 )
by ANPROJ_1:26;
not r1,p1,q1 are_collinear
by A2, ANPROJ_2:24;
then A12:
|{pp7,pp1,pp4}| <> 0
by A3, A6, A9, BKMODEL1:1;
|{pp7,pp1,pp4}| * |{pp7,pp8,pp9}| = 0
proof
now ( not p1,q1,p2 are_collinear & not p1,r1,p3 are_collinear & not p1,q1,p3 are_collinear & not q1,p1,p2 are_collinear & not p1,r1,p2 are_collinear & not p1,q1,q2 are_collinear & not p1,r1,r3 are_collinear & not q1,p1,q2 are_collinear & not r1,p1,r3 are_collinear & not p1,r1,q2 are_collinear & not p1,q1,r2 are_collinear & not p1,r1,q3 are_collinear & not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
p1,
q1,
p2 are_collinear & not
p1,
r1,
p3 are_collinear & not
p1,
q1,
p3 are_collinear )
by A1, Th4;
( not q1,p1,p2 are_collinear & not p1,r1,p2 are_collinear & not p1,q1,q2 are_collinear & not p1,r1,r3 are_collinear & not q1,p1,q2 are_collinear & not r1,p1,r3 are_collinear & not p1,r1,q2 are_collinear & not p1,q1,r2 are_collinear & not p1,r1,q3 are_collinear & not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )hence
not
q1,
p1,
p2 are_collinear
by ANPROJ_2:24;
( not p1,r1,p2 are_collinear & not p1,q1,q2 are_collinear & not p1,r1,r3 are_collinear & not q1,p1,q2 are_collinear & not r1,p1,r3 are_collinear & not p1,r1,q2 are_collinear & not p1,q1,r2 are_collinear & not p1,r1,q3 are_collinear & not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
p1,
r1,
p2 are_collinear & not
p1,
q1,
q2 are_collinear & not
p1,
r1,
r3 are_collinear )
by A1, Th4;
( not q1,p1,q2 are_collinear & not r1,p1,r3 are_collinear & not p1,r1,q2 are_collinear & not p1,q1,r2 are_collinear & not p1,r1,q3 are_collinear & not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )hence
( not
q1,
p1,
q2 are_collinear & not
r1,
p1,
r3 are_collinear )
by ANPROJ_2:24;
( not p1,r1,q2 are_collinear & not p1,q1,r2 are_collinear & not p1,r1,q3 are_collinear & not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
p1,
r1,
q2 are_collinear & not
p1,
q1,
r2 are_collinear & not
p1,
r1,
q3 are_collinear )
by A1, Th4;
( not p1,q1,q3 are_collinear & not p1,r1,r2 are_collinear & not q1,r1,q2 are_collinear & not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
p1,
q1,
q3 are_collinear & not
p1,
r1,
r2 are_collinear & not
q1,
r1,
q2 are_collinear )
by A1, Th4;
( not r1,p1,r2 are_collinear & not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )hence
not
r1,
p1,
r2 are_collinear
by ANPROJ_2:24;
( not q1,p1,q3 are_collinear & not q1,r1,r2 are_collinear & not q1,p1,p3 are_collinear & not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
q1,
p1,
q3 are_collinear & not
q1,
r1,
r2 are_collinear & not
q1,
p1,
p3 are_collinear )
by A1, Th4;
( not r1,q1,r2 are_collinear & not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )hence
not
r1,
q1,
r2 are_collinear
by ANPROJ_2:24;
( not q1,r1,p3 are_collinear & not q1,p1,r2 are_collinear & not q1,r1,p2 are_collinear & not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
q1,
r1,
p3 are_collinear & not
q1,
p1,
r2 are_collinear & not
q1,
r1,
p2 are_collinear )
by A1, Th4;
( not q1,p1,r3 are_collinear & not r1,p1,p2 are_collinear & not r1,q1,q3 are_collinear & not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
q1,
p1,
r3 are_collinear & not
r1,
p1,
p2 are_collinear & not
r1,
q1,
q3 are_collinear )
by A1, Th4;
( not p1,q1,r3 are_collinear & not q1,r1,q3 are_collinear & not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )hence
( not
p1,
q1,
r3 are_collinear & not
q1,
r1,
q3 are_collinear )
by ANPROJ_2:24;
( not r1,p1,q3 are_collinear & not r1,q1,p2 are_collinear & not r1,p1,q2 are_collinear & not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
r1,
p1,
q3 are_collinear & not
r1,
q1,
p2 are_collinear & not
r1,
p1,
q2 are_collinear )
by A1, Th4;
( not p1,r1,q3 are_collinear & not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
not
p1,
r1,
q3 are_collinear
by A1, Th4;
( not r1,q1,p3 are_collinear & not r1,p1,p3 are_collinear & not r1,q1,q2 are_collinear & not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
( not
r1,
q1,
p3 are_collinear & not
r1,
p1,
p3 are_collinear & not
r1,
q1,
q2 are_collinear )
by A1, Th4;
( not r1,q1,r3 are_collinear & not q1,r1,r3 are_collinear )thus
not
r1,
q1,
r3 are_collinear
by A1, Th5;
not q1,r1,r3 are_collinear hence
not
q1,
r1,
r3 are_collinear
by ANPROJ_2:24;
verum end;
then reconsider r142 =
|{pp1,pp4,pp2}|,
r173 =
|{pp1,pp7,pp3}|,
r143 =
|{pp1,pp4,pp3}|,
r172 =
|{pp1,pp7,pp2}|,
r145 =
|{pp1,pp4,pp5}|,
r179 =
|{pp1,pp7,pp9}|,
r149 =
|{pp1,pp4,pp9}|,
r175 =
|{pp1,pp7,pp5}|,
r148 =
|{pp1,pp4,pp8}|,
r176 =
|{pp1,pp7,pp6}|,
r146 =
|{pp1,pp4,pp6}|,
r178 =
|{pp1,pp7,pp8}|,
r475 =
|{pp4,pp7,pp5}|,
r416 =
|{pp4,pp1,pp6}|,
r476 =
|{pp4,pp7,pp6}|,
r415 =
|{pp4,pp1,pp5}|,
r478 =
|{pp4,pp7,pp8}|,
r413 =
|{pp4,pp1,pp3}|,
r473 =
|{pp4,pp7,pp3}|,
r418 =
|{pp4,pp1,pp8}|,
r472 =
|{pp4,pp7,pp2}|,
r419 =
|{pp4,pp1,pp9}|,
r479 =
|{pp4,pp7,pp9}|,
r412 =
|{pp4,pp1,pp2}|,
r712 =
|{pp7,pp1,pp2}|,
r746 =
|{pp7,pp4,pp6}|,
r716 =
|{pp7,pp1,pp6}|,
r742 =
|{pp7,pp4,pp2}|,
r715 =
|{pp7,pp1,pp5}|,
r743 =
|{pp7,pp4,pp3}|,
r713 =
|{pp7,pp1,pp3}|,
r745 =
|{pp7,pp4,pp5}|,
r749 =
|{pp7,pp4,pp9}|,
r718 =
|{pp7,pp1,pp8}|,
r719 =
|{pp7,pp1,pp9}|,
r748 =
|{pp7,pp4,pp8}| as non
zero Real by A3, A4, A5, A6, A7, A8, A9, A10, A11, BKMODEL1:1;
A13:
r718 * r749 = r719 * r748
proof
A14:
(
r142 * r173 = r143 * r172 &
r145 * r179 = r149 * r175 &
r148 * r176 = r146 * r178 &
r475 * r416 = r476 * r415 &
r478 * r413 = r473 * r418 &
r472 * r419 = r479 * r412 &
r712 * r746 = r716 * r742 &
r715 * r743 = r713 * r745 )
proof
A15:
(
p1,
p2,
p3 are_collinear &
p1,
q2,
r3 are_collinear &
p1,
r2,
q3 are_collinear &
q1,
q2,
q3 are_collinear )
by A1, Th6;
(
q1,
r2,
p3 are_collinear &
q1,
p2,
r3 are_collinear &
r1,
p2,
q3 are_collinear &
r1,
q2,
p3 are_collinear )
by A1, Th6;
hence
(
r142 * r173 = r143 * r172 &
r145 * r179 = r149 * r175 &
r148 * r176 = r146 * r178 &
r475 * r416 = r476 * r415 &
r478 * r413 = r473 * r418 &
r472 * r419 = r479 * r412 &
r712 * r746 = r716 * r742 &
r715 * r743 = r713 * r745 )
by A15, A3, A4, A11, A8, A10, A6, A5, A7, A9, Th2;
verum
end;
(
r146 = - r416 &
r145 = - r415 &
r143 = - r413 &
r148 = - r418 &
r149 = - r419 &
r142 = - r412 &
r172 = - r712 &
r476 = - r746 &
r176 = - r716 &
r472 = - r742 &
r175 = - r715 &
r473 = - r743 &
r173 = - r713 &
r475 = - r745 &
r478 = - r748 &
r479 = - r749 &
r178 = - r718 &
r179 = - r719 )
by ANPROJ_8:30;
hence
r718 * r749 = r719 * r748
by A14, Th3;
verum
end;
((|{pp7,pp1,pp4}| * |{pp7,pp8,pp9}|) - (|{pp7,pp1,pp8}| * |{pp7,pp4,pp9}|)) + (|{pp7,pp1,pp9}| * |{pp7,pp4,pp8}|) = 0
by ANPROJ_8:28;
hence
|{pp7,pp1,pp4}| * |{pp7,pp8,pp9}| = 0
by A13;
verum
end;
then
|{pp7,pp8,pp9}| = 0
by A12, XCMPLX_1:6;
hence
r1,r2,r3 are_collinear
by A9, A10, A11, BKMODEL1:1; verum