:: Desargues Theorem In Projective 3-Space :: by Eugeniusz Kusak :: :: Received August 13, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: PROJDES1:1 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c being Element of FCPS st a,b,c is_collinear holds ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) proofend; theorem :: PROJDES1:2 for FCPS being up-3-dimensional CollProjectiveSpace for p being Element of FCPS holds not for q, r being Element of FCPS holds p,q,r is_collinear proofend; theorem :: PROJDES1:3 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, b9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 holds not a,b9,c is_collinear proofend; theorem :: PROJDES1:4 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds a = d proofend; theorem Th5: :: PROJDES1:5 for FCPS being up-3-dimensional CollProjectiveSpace for o, a, d, d9, a9, s being Element of FCPS st not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,s is_collinear & o,a,a9 is_collinear & o <> a9 holds s <> d proofend; Lm1: for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, b9, c9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 holds b9 <> c9 proofend; definition let FCPS be up-3-dimensional CollProjectiveSpace; let a, b, c, d be Element of FCPS; preda,b,c,d are_coplanar means :Def1: :: PROJDES1:def 1 ex x being Element of FCPS st ( a,b,x is_collinear & c,d,x is_collinear ); end; :: deftheorem Def1 defines are_coplanar PROJDES1:def_1_:_ for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS holds ( a,b,c,d are_coplanar iff ex x being Element of FCPS st ( a,b,x is_collinear & c,d,x is_collinear ) ); theorem Th6: :: PROJDES1:6 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) holds a,b,c,d are_coplanar proofend; Lm2: for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds b,a,c,d are_coplanar proofend; Lm3: for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds b,c,d,a are_coplanar proofend; theorem Th7: :: PROJDES1:7 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar ) proofend; Lm4: for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, p, q being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds a,b,p,q are_coplanar proofend; theorem Th8: :: PROJDES1:8 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, p, q, r, s being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar holds p,q,r,s are_coplanar proofend; Lm5: for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, p, q, r being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar holds a,p,q,r are_coplanar proofend; theorem :: PROJDES1:9 for FCPS being up-3-dimensional CollProjectiveSpace for p, q, r, a, b, c, s being Element of FCPS st not p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,r are_coplanar & a,b,c,q are_coplanar & p,q,r,s are_coplanar holds a,b,c,s are_coplanar proofend; Lm6: for FCPS being up-3-dimensional CollProjectiveSpace for p, q, r, a, b being Element of FCPS st p <> q & p,q,r is_collinear & a,b,p,q are_coplanar holds a,b,p,r are_coplanar proofend; theorem Th10: :: PROJDES1:10 for FCPS being up-3-dimensional CollProjectiveSpace for p, q, r, a, b, c being Element of FCPS st p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds a,b,c,r are_coplanar proofend; theorem :: PROJDES1:11 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, p, q, r, s being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar holds ex x being Element of FCPS st ( p,q,x is_collinear & r,s,x is_collinear ) proofend; theorem Th12: :: PROJDES1:12 for FCPS being up-3-dimensional CollProjectiveSpace holds not for a, b, c, d being Element of FCPS holds a,b,c,d are_coplanar proofend; theorem Th13: :: PROJDES1:13 for FCPS being up-3-dimensional CollProjectiveSpace for p, q, r being Element of FCPS st not p,q,r is_collinear holds ex s being Element of FCPS st not p,q,r,s are_coplanar proofend; theorem Th14: :: PROJDES1:14 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d being Element of FCPS st ( a = b or a = c or b = c or a = d or b = d or d = c ) holds a,b,c,d are_coplanar proofend; theorem Th15: :: PROJDES1:15 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, o, a9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & a <> a9 holds not a,b,c,a9 are_coplanar proofend; theorem Th16: :: PROJDES1:16 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, a9, b9, c9, p, q, r being Element of FCPS st not a,b,c is_collinear & not a9,b9,c9 is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar holds p,q,r is_collinear proofend; theorem Th17: :: PROJDES1:17 for FCPS being up-3-dimensional CollProjectiveSpace for a, a9, o, b, c, b9, c9, p, q, r being Element of FCPS st a <> a9 & o,a,a9 is_collinear & not a,b,c,o are_coplanar & not a9,b9,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds p,q,r is_collinear proofend; theorem Th18: :: PROJDES1:18 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, d, o being Element of FCPS st not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear holds not a,b,d,o are_coplanar proofend; theorem Th19: :: PROJDES1:19 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, o, a9, b9, c9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & o <> a9 & o <> b9 & o <> c9 holds ( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar ) proofend; theorem Th20: :: PROJDES1:20 for FCPS being up-3-dimensional CollProjectiveSpace for a, b, c, o, d, d9, a9, b9, s, t, u being Element of FCPS st a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & a,d,s is_collinear & a9,d9,s is_collinear & b,d,t is_collinear & b9,d9,t is_collinear & c,d,u is_collinear & o <> a9 & d <> d9 & o <> b9 holds not s,t,u is_collinear proofend; definition let FCPS be up-3-dimensional CollProjectiveSpace; let o, a, b, c be Element of FCPS; predo,a,b,c constitute_a_quadrangle means :Def2: :: PROJDES1:def 2 ( not a,b,c is_collinear & not o,a,b is_collinear & not o,b,c is_collinear & not o,c,a is_collinear ); end; :: deftheorem Def2 defines constitute_a_quadrangle PROJDES1:def_2_:_ for FCPS being up-3-dimensional CollProjectiveSpace for o, a, b, c being Element of FCPS holds ( o,a,b,c constitute_a_quadrangle iff ( not a,b,c is_collinear & not o,a,b is_collinear & not o,b,c is_collinear & not o,c,a is_collinear ) ); Lm7: for FCPS being up-3-dimensional CollProjectiveSpace for o, a9, b9, c9, a, b, c, p, q, r being Element of FCPS st o <> a9 & o <> b9 & o <> c9 & a <> a9 & b <> b9 & o,a,b,c constitute_a_quadrangle & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds p,q,r is_collinear proofend; theorem Th21: :: PROJDES1:21 for FCPS being up-3-dimensional CollProjectiveSpace for o, a, b, c, a9, b9, c9, p, r, q being Element of FCPS st not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & a <> a9 & b,c,r is_collinear & b9,c9,r is_collinear & a,c,q is_collinear & b <> b9 & a9,c9,q is_collinear & o <> a9 & o <> b9 & o <> c9 holds r,q,p is_collinear proofend; theorem Th22: :: PROJDES1:22 for CS being up-3-dimensional CollProjectiveSpace holds CS is Desarguesian proofend; registration clusterV38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional -> Desarguesian up-3-dimensional for L13(); correctness coherence for b1 being up-3-dimensional CollProjectiveSpace holds b1 is Desarguesian ; by Th22; end;