:: Desargues Theorem In Projective 3-Space :: by Eugeniusz Kusak :: :: Received August 13, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INCSP_1, ANPROJ_2, SUBSET_1, AFF_2, PROJDES1, PENCIL_1; notations STRUCT_0, COLLSP, ANPROJ_2; constructors ANPROJ_2, COLLSP; registrations ANPROJ_2; begin reserve FCPS for up-3-dimensional CollProjectiveSpace; reserve a,a9,b,b9,c,c9,d,d9,o,p,q,r,s,t,u,x,y,z for Element of FCPS; theorem :: PROJDES1:1 a,b,c are_collinear implies b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear; theorem :: PROJDES1:2 ex q,r st not p,q,r are_collinear; theorem :: PROJDES1:3 not a,b,c are_collinear & a,b,b9 are_collinear & a<>b9 implies not a,b9, c are_collinear; theorem :: PROJDES1:4 not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear implies a=d; theorem :: PROJDES1:5 not o,a,d are_collinear & o,d,d9 are_collinear & d<>d9 & a9,d9,s are_collinear & o,a,a9 are_collinear & o<>a9 implies s<>d; definition let FCPS,a,b,c,d; pred a,b,c,d are_coplanar means :: PROJDES1:def 1 ex x being Element of FCPS st a,b,x are_collinear & c,d,x are_collinear; end; theorem :: PROJDES1:6 a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear implies a,b,c,d are_coplanar; theorem :: PROJDES1:7 a,b,c,d are_coplanar implies 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; theorem :: PROJDES1:8 not a,b,c are_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 implies p,q,r,s are_coplanar; theorem :: PROJDES1:9 not p,q,r are_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 implies a,b,c,s are_coplanar; theorem :: PROJDES1:10 p<>q & p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar implies a,b,c,r are_coplanar; theorem :: PROJDES1:11 not a,b,c are_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 implies ex x st p,q,x are_collinear & r,s,x are_collinear; theorem :: PROJDES1:12 ex a,b,c,d st not a,b,c,d are_coplanar; theorem :: PROJDES1:13 not p,q,r are_collinear implies ex s st not p,q,r,s are_coplanar; theorem :: PROJDES1:14 a=b or a=c or b=c or a=d or b=d or d=c implies a,b,c,d are_coplanar; theorem :: PROJDES1:15 not a,b,c,o are_coplanar & o,a,a9 are_collinear & a<>a9 implies not a,b,c,a9 are_coplanar; theorem :: PROJDES1:16 not a,b,c are_collinear & not a9,b9,c9 are_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 implies p,q,r are_collinear; theorem :: PROJDES1:17 a<>a9 & o,a,a9 are_collinear & not a,b,c,o are_coplanar & not a9, b9,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & b,c,q are_collinear & b9,c9,q are_collinear & a,c,r are_collinear & a9,c9,r are_collinear implies p,q,r are_collinear; theorem :: PROJDES1:18 not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o are_collinear implies not a,b,d,o are_coplanar; theorem :: PROJDES1:19 not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & o<>a9 & o<>b9 & o<>c9 implies not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar; theorem :: PROJDES1:20 a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & a,d,s are_collinear & a9,d9,s are_collinear & b,d,t are_collinear & b9,d9,t are_collinear & c,d,u are_collinear & o<>a9 & d<>d9 & o<>b9 implies not s,t,u are_collinear; definition let FCPS,o,a,b,c; pred o,a,b,c constitute_a_quadrangle means :: PROJDES1:def 2 not a,b,c are_collinear & not o,a,b are_collinear & not o,b,c are_collinear & not o,c,a are_collinear; end; theorem :: PROJDES1:21 not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & a<>a9 & b,c,r are_collinear & b9, c9,r are_collinear & a,c,q are_collinear & b<>b9 & a9,c9,q are_collinear & o<>a9 & o<>b9 & o<>c9 implies r,q,p are_collinear; theorem :: PROJDES1:22 for CS being up-3-dimensional CollProjectiveSpace holds CS is Desarguesian; registration cluster -> Desarguesian for up-3-dimensional CollProjectiveSpace; end;