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

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

assume that

A1: o <> p2 and

A2: o <> p3 and

A3: p2 <> p3 and

A4: p1 <> p2 and

A5: p1 <> p3 and

A6: o <> q2 and

A7: o <> q3 and

A8: q2 <> q3 and

A9: q1 <> q2 and

A10: q1 <> q3 and

A11: not o,p1,q1 are_collinear and

A12: o,p1,p2 are_collinear and

A13: o,p1,p3 are_collinear and

A14: o,q1,q2 are_collinear and

A15: o,q1,q3 are_collinear and

A16: p1,q2,r3 are_collinear and

A17: q1,p2,r3 are_collinear and

A18: p1,q3,r2 are_collinear and

A19: p3,q1,r2 are_collinear and

A20: p2,q3,r1 are_collinear and

A21: p3,q2,r1 are_collinear ; :: thesis: r1,r2,r3 are_collinear

consider o999, q19, q29 being Element of V such that

A22: o = Dir o999 and

A23: q1 = Dir q19 and

A24: q2 = Dir q29 and

A25: not o999 is zero and

A26: not q19 is zero and

A27: not q29 is zero and

A28: o999,q19,q29 are_LinDep by A14, Th23;

A29: not are_Prop q19,q29 by A9, A23, A24, A26, A27, ANPROJ_1:22;

consider o9999, q199, q39 being Element of V such that

A30: o = Dir o9999 and

A31: q1 = Dir q199 and

A32: q3 = Dir q39 and

A33: not o9999 is zero and

A34: not q199 is zero and

A35: not q39 is zero and

A36: o9999,q199,q39 are_LinDep by A15, Th23;

A37: are_Prop q199,q19 by A23, A26, A31, A34, ANPROJ_1:22;

consider o99, p199, p39 being Element of V such that

A38: ( o = Dir o99 & p1 = Dir p199 ) and

A39: p3 = Dir p39 and

A40: ( not o99 is zero & not p199 is zero ) and

A41: not p39 is zero and

A42: o99,p199,p39 are_LinDep by A13, Th23;

consider o9, p19, p29 being Element of V such that

A43: o = Dir o9 and

A44: p1 = Dir p19 and

A45: p2 = Dir p29 and

A46: not o9 is zero and

A47: not p19 is zero and

A48: not p29 is zero and

A49: o9,p19,p29 are_LinDep by A12, Th23;

A50: ( not are_Prop o9,p39 & not are_Prop p19,p39 ) by A2, A5, A43, A44, A46, A47, A39, A41, ANPROJ_1:22;

A51: ( not are_Prop q19,q39 & not are_Prop q29,q39 ) by A8, A10, A23, A24, A26, A27, A32, A35, ANPROJ_1:22;

A52: not are_Prop p29,p39 by A3, A45, A48, A39, A41, ANPROJ_1:22;

A53: not are_Prop o9,q39 by A7, A43, A46, A32, A35, ANPROJ_1:22;

A54: not are_Prop o9,q29 by A6, A43, A46, A24, A27, ANPROJ_1:22;

( not are_Prop o9,p29 & not are_Prop p19,p29 ) by A1, A4, A43, A44, A45, A46, A47, A48, ANPROJ_1:22;

then A55: o9,p19,p29,p39,q19,q29,q39 are_half_mutually_not_Prop by A54, A53, A50, A29, A52, A51;

consider q1999, p2999, r399 being Element of V such that

A56: q1 = Dir q1999 and

A57: p2 = Dir p2999 and

A58: r3 = Dir r399 and

A59: not q1999 is zero and

A60: not p2999 is zero and

A61: not r399 is zero and

A62: q1999,p2999,r399 are_LinDep by A17, Th23;

A63: are_Prop q1999,q19 by A23, A26, A56, A59, ANPROJ_1:22;

consider p29999, q3999, r19 being Element of V such that

A64: p2 = Dir p29999 and

A65: q3 = Dir q3999 and

A66: r1 = Dir r19 and

A67: not p29999 is zero and

A68: not q3999 is zero and

A69: not r19 is zero and

A70: p29999,q3999,r19 are_LinDep by A20, Th23;

A71: are_Prop q3999,q39 by A32, A35, A65, A68, ANPROJ_1:22;

are_Prop o999,o9 by A43, A46, A22, A25, ANPROJ_1:22;

then A72: o9,q19,q29 are_LinDep by A28, ANPROJ_1:4;

are_Prop o9999,o9 by A43, A46, A30, A33, ANPROJ_1:22;

then A73: o9,q19,q39 are_LinDep by A36, A37, ANPROJ_1:4;

( are_Prop o99,o9 & are_Prop p199,p19 ) by A43, A44, A46, A47, A38, A40, ANPROJ_1:22;

then A74: o9,p19,p39 are_LinDep by A42, ANPROJ_1:4;

not o9,p19,q19 are_LinDep by A11, A43, A44, A46, A47, A23, A26, Th23;

then A75: o9,p19,p29,p39,q19,q29,q39 lie_on_an_angle by A49, A74, A72, A73;

consider p19999, q399, r29 being Element of V such that

A76: p1 = Dir p19999 and

A77: q3 = Dir q399 and

A78: r2 = Dir r29 and

A79: not p19999 is zero and

A80: not q399 is zero and

A81: not r29 is zero and

A82: p19999,q399,r29 are_LinDep by A18, Th23;

A83: are_Prop q399,q39 by A32, A35, A77, A80, ANPROJ_1:22;

consider p3999, q29999, r199 being Element of V such that

A84: p3 = Dir p3999 and

A85: q2 = Dir q29999 and

A86: r1 = Dir r199 and

A87: not p3999 is zero and

A88: not q29999 is zero and

A89: not r199 is zero and

A90: p3999,q29999,r199 are_LinDep by A21, Th23;

A91: are_Prop p3999,p39 by A39, A41, A84, A87, ANPROJ_1:22;

A92: are_Prop q29999,q29 by A24, A27, A85, A88, ANPROJ_1:22;

are_Prop r199,r19 by A66, A69, A86, A89, ANPROJ_1:22;

then A93: p39,q29,r19 are_LinDep by A90, A91, A92, ANPROJ_1:4;

A94: q19,q29,q39 are_Prop_Vect by A26, A27, A35;

A95: p19,p29,p39 are_Prop_Vect by A47, A48, A41;

are_Prop p29999,p29 by A45, A48, A64, A67, ANPROJ_1:22;

then A96: p29,q39,r19 are_LinDep by A70, A71, ANPROJ_1:4;

consider p399, q1999, r299 being Element of V such that

A97: p3 = Dir p399 and

A98: q1 = Dir q1999 and

A99: r2 = Dir r299 and

A100: not p399 is zero and

A101: not q1999 is zero and

A102: not r299 is zero and

A103: p399,q1999,r299 are_LinDep by A19, Th23;

A104: are_Prop q1999,q19 by A23, A26, A98, A101, ANPROJ_1:22;

are_Prop p19999,p19 by A44, A47, A76, A79, ANPROJ_1:22;

then A105: p19,q39,r29 are_LinDep by A82, A83, ANPROJ_1:4;

consider p1999, q2999, r39 being Element of V such that

A106: p1 = Dir p1999 and

A107: q2 = Dir q2999 and

A108: r3 = Dir r39 and

A109: not p1999 is zero and

A110: not q2999 is zero and

A111: not r39 is zero and

A112: p1999,q2999,r39 are_LinDep by A16, Th23;

A113: are_Prop q2999,q29 by A24, A27, A107, A110, ANPROJ_1:22;

A114: are_Prop p2999,p29 by A45, A48, A57, A60, ANPROJ_1:22;

are_Prop r399,r39 by A108, A111, A58, A61, ANPROJ_1:22;

then A115: q19,p29,r39 are_LinDep by A62, A63, A114, ANPROJ_1:4;

are_Prop p1999,p19 by A44, A47, A106, A109, ANPROJ_1:22;

then A116: p19,q29,r39 are_LinDep by A112, A113, ANPROJ_1:4;

A117: are_Prop p399,p39 by A39, A41, A97, A100, ANPROJ_1:22;

are_Prop r299,r29 by A78, A81, A99, A102, ANPROJ_1:22;

then A118: p39,q19,r29 are_LinDep by A103, A117, A104, ANPROJ_1:4;

r19,r29,r39 are_Prop_Vect by A111, A81, A69;

then r19,r29,r39 are_LinDep by A46, A75, A55, A95, A94, A116, A115, A105, A118, A96, A93, Th9;

hence r1,r2,r3 are_collinear by A108, A111, A78, A81, A66, A69, Th23; :: thesis: verum

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

assume that

A1: o <> p2 and

A2: o <> p3 and

A3: p2 <> p3 and

A4: p1 <> p2 and

A5: p1 <> p3 and

A6: o <> q2 and

A7: o <> q3 and

A8: q2 <> q3 and

A9: q1 <> q2 and

A10: q1 <> q3 and

A11: not o,p1,q1 are_collinear and

A12: o,p1,p2 are_collinear and

A13: o,p1,p3 are_collinear and

A14: o,q1,q2 are_collinear and

A15: o,q1,q3 are_collinear and

A16: p1,q2,r3 are_collinear and

A17: q1,p2,r3 are_collinear and

A18: p1,q3,r2 are_collinear and

A19: p3,q1,r2 are_collinear and

A20: p2,q3,r1 are_collinear and

A21: p3,q2,r1 are_collinear ; :: thesis: r1,r2,r3 are_collinear

consider o999, q19, q29 being Element of V such that

A22: o = Dir o999 and

A23: q1 = Dir q19 and

A24: q2 = Dir q29 and

A25: not o999 is zero and

A26: not q19 is zero and

A27: not q29 is zero and

A28: o999,q19,q29 are_LinDep by A14, Th23;

A29: not are_Prop q19,q29 by A9, A23, A24, A26, A27, ANPROJ_1:22;

consider o9999, q199, q39 being Element of V such that

A30: o = Dir o9999 and

A31: q1 = Dir q199 and

A32: q3 = Dir q39 and

A33: not o9999 is zero and

A34: not q199 is zero and

A35: not q39 is zero and

A36: o9999,q199,q39 are_LinDep by A15, Th23;

A37: are_Prop q199,q19 by A23, A26, A31, A34, ANPROJ_1:22;

consider o99, p199, p39 being Element of V such that

A38: ( o = Dir o99 & p1 = Dir p199 ) and

A39: p3 = Dir p39 and

A40: ( not o99 is zero & not p199 is zero ) and

A41: not p39 is zero and

A42: o99,p199,p39 are_LinDep by A13, Th23;

consider o9, p19, p29 being Element of V such that

A43: o = Dir o9 and

A44: p1 = Dir p19 and

A45: p2 = Dir p29 and

A46: not o9 is zero and

A47: not p19 is zero and

A48: not p29 is zero and

A49: o9,p19,p29 are_LinDep by A12, Th23;

A50: ( not are_Prop o9,p39 & not are_Prop p19,p39 ) by A2, A5, A43, A44, A46, A47, A39, A41, ANPROJ_1:22;

A51: ( not are_Prop q19,q39 & not are_Prop q29,q39 ) by A8, A10, A23, A24, A26, A27, A32, A35, ANPROJ_1:22;

A52: not are_Prop p29,p39 by A3, A45, A48, A39, A41, ANPROJ_1:22;

A53: not are_Prop o9,q39 by A7, A43, A46, A32, A35, ANPROJ_1:22;

A54: not are_Prop o9,q29 by A6, A43, A46, A24, A27, ANPROJ_1:22;

( not are_Prop o9,p29 & not are_Prop p19,p29 ) by A1, A4, A43, A44, A45, A46, A47, A48, ANPROJ_1:22;

then A55: o9,p19,p29,p39,q19,q29,q39 are_half_mutually_not_Prop by A54, A53, A50, A29, A52, A51;

consider q1999, p2999, r399 being Element of V such that

A56: q1 = Dir q1999 and

A57: p2 = Dir p2999 and

A58: r3 = Dir r399 and

A59: not q1999 is zero and

A60: not p2999 is zero and

A61: not r399 is zero and

A62: q1999,p2999,r399 are_LinDep by A17, Th23;

A63: are_Prop q1999,q19 by A23, A26, A56, A59, ANPROJ_1:22;

consider p29999, q3999, r19 being Element of V such that

A64: p2 = Dir p29999 and

A65: q3 = Dir q3999 and

A66: r1 = Dir r19 and

A67: not p29999 is zero and

A68: not q3999 is zero and

A69: not r19 is zero and

A70: p29999,q3999,r19 are_LinDep by A20, Th23;

A71: are_Prop q3999,q39 by A32, A35, A65, A68, ANPROJ_1:22;

are_Prop o999,o9 by A43, A46, A22, A25, ANPROJ_1:22;

then A72: o9,q19,q29 are_LinDep by A28, ANPROJ_1:4;

are_Prop o9999,o9 by A43, A46, A30, A33, ANPROJ_1:22;

then A73: o9,q19,q39 are_LinDep by A36, A37, ANPROJ_1:4;

( are_Prop o99,o9 & are_Prop p199,p19 ) by A43, A44, A46, A47, A38, A40, ANPROJ_1:22;

then A74: o9,p19,p39 are_LinDep by A42, ANPROJ_1:4;

not o9,p19,q19 are_LinDep by A11, A43, A44, A46, A47, A23, A26, Th23;

then A75: o9,p19,p29,p39,q19,q29,q39 lie_on_an_angle by A49, A74, A72, A73;

consider p19999, q399, r29 being Element of V such that

A76: p1 = Dir p19999 and

A77: q3 = Dir q399 and

A78: r2 = Dir r29 and

A79: not p19999 is zero and

A80: not q399 is zero and

A81: not r29 is zero and

A82: p19999,q399,r29 are_LinDep by A18, Th23;

A83: are_Prop q399,q39 by A32, A35, A77, A80, ANPROJ_1:22;

consider p3999, q29999, r199 being Element of V such that

A84: p3 = Dir p3999 and

A85: q2 = Dir q29999 and

A86: r1 = Dir r199 and

A87: not p3999 is zero and

A88: not q29999 is zero and

A89: not r199 is zero and

A90: p3999,q29999,r199 are_LinDep by A21, Th23;

A91: are_Prop p3999,p39 by A39, A41, A84, A87, ANPROJ_1:22;

A92: are_Prop q29999,q29 by A24, A27, A85, A88, ANPROJ_1:22;

are_Prop r199,r19 by A66, A69, A86, A89, ANPROJ_1:22;

then A93: p39,q29,r19 are_LinDep by A90, A91, A92, ANPROJ_1:4;

A94: q19,q29,q39 are_Prop_Vect by A26, A27, A35;

A95: p19,p29,p39 are_Prop_Vect by A47, A48, A41;

are_Prop p29999,p29 by A45, A48, A64, A67, ANPROJ_1:22;

then A96: p29,q39,r19 are_LinDep by A70, A71, ANPROJ_1:4;

consider p399, q1999, r299 being Element of V such that

A97: p3 = Dir p399 and

A98: q1 = Dir q1999 and

A99: r2 = Dir r299 and

A100: not p399 is zero and

A101: not q1999 is zero and

A102: not r299 is zero and

A103: p399,q1999,r299 are_LinDep by A19, Th23;

A104: are_Prop q1999,q19 by A23, A26, A98, A101, ANPROJ_1:22;

are_Prop p19999,p19 by A44, A47, A76, A79, ANPROJ_1:22;

then A105: p19,q39,r29 are_LinDep by A82, A83, ANPROJ_1:4;

consider p1999, q2999, r39 being Element of V such that

A106: p1 = Dir p1999 and

A107: q2 = Dir q2999 and

A108: r3 = Dir r39 and

A109: not p1999 is zero and

A110: not q2999 is zero and

A111: not r39 is zero and

A112: p1999,q2999,r39 are_LinDep by A16, Th23;

A113: are_Prop q2999,q29 by A24, A27, A107, A110, ANPROJ_1:22;

A114: are_Prop p2999,p29 by A45, A48, A57, A60, ANPROJ_1:22;

are_Prop r399,r39 by A108, A111, A58, A61, ANPROJ_1:22;

then A115: q19,p29,r39 are_LinDep by A62, A63, A114, ANPROJ_1:4;

are_Prop p1999,p19 by A44, A47, A106, A109, ANPROJ_1:22;

then A116: p19,q29,r39 are_LinDep by A112, A113, ANPROJ_1:4;

A117: are_Prop p399,p39 by A39, A41, A97, A100, ANPROJ_1:22;

are_Prop r299,r29 by A78, A81, A99, A102, ANPROJ_1:22;

then A118: p39,q19,r29 are_LinDep by A103, A117, A104, ANPROJ_1:4;

r19,r29,r39 are_Prop_Vect by A111, A81, A69;

then r19,r29,r39 are_LinDep by A46, A75, A55, A95, A94, A116, A115, A105, A118, A96, A93, Th9;

hence r1,r2,r3 are_collinear by A108, A111, A78, A81, A66, A69, Th23; :: thesis: verum