let V be up-3-dimensional RealLinearSpace; :: thesis: ProjectiveSpace V is Desarguesian

let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 12 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 12 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum