let V be up-3-dimensional RealLinearSpace; ProjectiveSpace V is Desarguesian
let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace V); ANPROJ_2:def 12 ( o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1:
o <> q1
and
A2:
p1 <> q1
and
A3:
o <> q2
and
A4:
p2 <> q2
and
A5:
o <> q3
and
A6:
p3 <> q3
and
A7:
not o,p1,p2 are_collinear
and
A8:
( not o,p1,p3 are_collinear & not o,p2,p3 are_collinear )
and
A9:
p1,p2,r3 are_collinear
and
A10:
q1,q2,r3 are_collinear
and
A11:
p2,p3,r1 are_collinear
and
A12:
q2,q3,r1 are_collinear
and
A13:
p1,p3,r2 are_collinear
and
A14:
q1,q3,r2 are_collinear
and
A15:
o,p1,q1 are_collinear
and
A16:
o,p2,q2 are_collinear
and
A17:
o,p3,q3 are_collinear
; r1,r2,r3 are_collinear
consider q19, q29, r399 being Element of V such that
A18:
q1 = Dir q19
and
A19:
q2 = Dir q29
and
A20:
r3 = Dir r399
and
A21:
not q19 is zero
and
A22:
not q29 is zero
and
A23:
not r399 is zero
and
A24:
q19,q29,r399 are_LinDep
by A10, Th23;
consider q299, q39, r199 being Element of V such that
A25:
q2 = Dir q299
and
A26:
q3 = Dir q39
and
A27:
r1 = Dir r199
and
A28:
not q299 is zero
and
A29:
not q39 is zero
and
A30:
not r199 is zero
and
A31:
q299,q39,r199 are_LinDep
by A12, Th23;
A32:
are_Prop q299,q29
by A19, A22, A25, A28, ANPROJ_1:22;
consider p299, p39, r19 being Element of V such that
A33:
p2 = Dir p299
and
A34:
p3 = Dir p39
and
A35:
r1 = Dir r19
and
A36:
not p299 is zero
and
A37:
not p39 is zero
and
A38:
not r19 is zero
and
A39:
p299,p39,r19 are_LinDep
by A11, Th23;
A40:
not are_Prop p39,q39
by A6, A34, A37, A26, A29, ANPROJ_1:22;
are_Prop r199,r19
by A35, A38, A27, A30, ANPROJ_1:22;
then A41:
q29,q39,r19 are_LinDep
by A31, A32, ANPROJ_1:4;
consider p199, p399, r29 being Element of V such that
A42:
p1 = Dir p199
and
A43:
p3 = Dir p399
and
A44:
r2 = Dir r29
and
A45:
not p199 is zero
and
A46:
not p399 is zero
and
A47:
not r29 is zero
and
A48:
p199,p399,r29 are_LinDep
by A13, Th23;
A49:
are_Prop p399,p39
by A34, A37, A43, A46, ANPROJ_1:22;
consider o9 being Element of V such that
A50:
not o9 is zero
and
A51:
o = Dir o9
by ANPROJ_1:26;
A52:
not are_Prop o9,q39
by A5, A50, A51, A26, A29, ANPROJ_1:22;
consider p19, p29, r39 being Element of V such that
A53:
p1 = Dir p19
and
A54:
p2 = Dir p29
and
A55:
r3 = Dir r39
and
A56:
not p19 is zero
and
A57:
not p29 is zero
and
A58:
not r39 is zero
and
A59:
p19,p29,r39 are_LinDep
by A9, Th23;
A60:
( not are_Prop p19,q19 & not are_Prop p29,q29 )
by A2, A4, A53, A54, A56, A57, A18, A19, A21, A22, ANPROJ_1:22;
A61:
( not are_Prop o9,q19 & not are_Prop o9,q29 )
by A1, A3, A50, A51, A18, A19, A21, A22, ANPROJ_1:22;
consider o999, p2999, q2999 being Element of V such that
A62:
o = Dir o999
and
A63:
p2 = Dir p2999
and
A64:
q2 = Dir q2999
and
A65:
not o999 is zero
and
A66:
not p2999 is zero
and
A67:
not q2999 is zero
and
A68:
o999,p2999,q2999 are_LinDep
by A16, Th23;
A69:
are_Prop q2999,q29
by A19, A22, A64, A67, ANPROJ_1:22;
A70:
are_Prop o999,o9
by A50, A51, A62, A65, ANPROJ_1:22;
are_Prop p2999,p29
by A54, A57, A63, A66, ANPROJ_1:22;
then A71:
o9,p29,q29 are_LinDep
by A68, A70, A69, ANPROJ_1:4;
consider q199, q399, r299 being Element of V such that
A72:
q1 = Dir q199
and
A73:
q3 = Dir q399
and
A74:
r2 = Dir r299
and
A75:
not q199 is zero
and
A76:
not q399 is zero
and
A77:
not r299 is zero
and
A78:
q199,q399,r299 are_LinDep
by A14, Th23;
A79:
are_Prop q199,q19
by A18, A21, A72, A75, ANPROJ_1:22;
A80:
not o9,p19,p29 are_LinDep
by A7, A50, A51, A53, A54, A56, A57, Th23;
are_Prop r399,r39
by A55, A58, A20, A23, ANPROJ_1:22;
then A81:
q19,q29,r39 are_LinDep
by A24, ANPROJ_1:4;
A82:
are_Prop q399,q39
by A26, A29, A73, A76, ANPROJ_1:22;
consider o9999, p3999, q3999 being Element of V such that
A83:
o = Dir o9999
and
A84:
p3 = Dir p3999
and
A85:
q3 = Dir q3999
and
A86:
not o9999 is zero
and
A87:
not p3999 is zero
and
A88:
not q3999 is zero
and
A89:
o9999,p3999,q3999 are_LinDep
by A17, Th23;
A90:
are_Prop q3999,q39
by A26, A29, A85, A88, ANPROJ_1:22;
are_Prop p299,p29
by A54, A57, A33, A36, ANPROJ_1:22;
then A91:
p29,p39,r19 are_LinDep
by A39, ANPROJ_1:4;
are_Prop p199,p19
by A53, A56, A42, A45, ANPROJ_1:22;
then
p19,p39,r29 are_LinDep
by A48, A49, ANPROJ_1:4;
then A92:
p19,p29,p39,r19,r29,r39 lie_on_a_triangle
by A59, A91;
A93:
q19,q29,q39 are_Prop_Vect
by A21, A22, A29;
consider o99, p1999, q1999 being Element of V such that
A94:
o = Dir o99
and
A95:
p1 = Dir p1999
and
A96:
q1 = Dir q1999
and
A97:
not o99 is zero
and
A98:
not p1999 is zero
and
A99:
not q1999 is zero
and
A100:
o99,p1999,q1999 are_LinDep
by A15, Th23;
A101:
are_Prop q1999,q19
by A18, A21, A96, A99, ANPROJ_1:22;
A102:
( not o9,p19,p39 are_LinDep & not o9,p29,p39 are_LinDep )
by A8, A50, A51, A53, A54, A56, A57, A34, A37, Th23;
A103:
p19,p29,p39 are_Prop_Vect
by A56, A57, A37;
A104:
are_Prop o9999,o9
by A50, A51, A83, A86, ANPROJ_1:22;
are_Prop p3999,p39
by A34, A37, A84, A87, ANPROJ_1:22;
then A105:
o9,p39,q39 are_LinDep
by A89, A104, A90, ANPROJ_1:4;
A106:
are_Prop o99,o9
by A50, A51, A94, A97, ANPROJ_1:22;
are_Prop p1999,p19
by A53, A56, A95, A98, ANPROJ_1:22;
then
o9,p19,q19 are_LinDep
by A100, A106, A101, ANPROJ_1:4;
then A107:
o9,p19,p29,p39,q19,q29,q39 are_perspective
by A71, A105;
are_Prop r299,r29
by A44, A47, A74, A77, ANPROJ_1:22;
then
q19,q39,r29 are_LinDep
by A78, A79, A82, ANPROJ_1:4;
then A108:
q19,q29,q39,r19,r29,r39 lie_on_a_triangle
by A81, A41;
r19,r29,r39 are_Prop_Vect
by A58, A38, A47;
then
r19,r29,r39 are_LinDep
by A50, A61, A52, A60, A40, A103, A93, A107, A80, A102, A92, A108, Th8;
hence
r1,r2,r3 are_collinear
by A55, A58, A35, A38, A44, A47, Th23; verum