Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Desargues Theorem In Projective 3-Space

by
Eugeniusz Kusak

MML identifier: PROJDES1
[ Mizar article, MML identifier index ]

```environ

vocabulary ANPROJ_2, INCSP_1, AFF_2, PROJDES1;
notation STRUCT_0, COLLSP, ANPROJ_2;
constructors ANPROJ_2, XBOOLE_0;
clusters ANPROJ_2, ZFMISC_1, XBOOLE_0;

begin

reserve FCPS for up-3-dimensional CollProjectiveSpace;
reserve a,a',b,b',c,c',d,d',o,p,q,r,s,t,u,x,y,z
for Element of FCPS;

theorem :: PROJDES1:1
a,b,c is_collinear implies 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;

canceled 3;

theorem :: PROJDES1:5
ex q,r st not p,q,r is_collinear;

theorem :: PROJDES1:6
not a,b,c is_collinear & a,b,b' is_collinear & a<>b' implies
not a,b',c is_collinear;

theorem :: PROJDES1:7
not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear
implies a=d;

theorem :: PROJDES1:8
not o,a,d is_collinear & o,d,d' is_collinear & a,d,s is_collinear &
d<>d' & a',d',s is_collinear & o,a,a' is_collinear & o<>a' 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 is_collinear & c,d,x is_collinear;
end;

canceled;

theorem :: PROJDES1:10
a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or
d,a,b is_collinear implies a,b,c,d are_coplanar;

theorem :: PROJDES1:11
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:12
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 implies p,q,r,s are_coplanar;

theorem :: PROJDES1:13
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 implies a,b,c,s are_coplanar
;

theorem :: PROJDES1:14
p<>q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar
implies a,b,c,r are_coplanar;

theorem :: PROJDES1:15
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 implies ex x st p,q,x is_collinear
& r,s,x is_collinear;

theorem :: PROJDES1:16
ex a,b,c,d st not a,b,c,d are_coplanar;

theorem :: PROJDES1:17
not p,q,r is_collinear implies ex s st not p,q,r,s are_coplanar;

theorem :: PROJDES1:18
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:19
not a,b,c,o are_coplanar & o,a,a' is_collinear & a<>a' implies not
a,b,c,a' are_coplanar;

theorem :: PROJDES1:20
not a,b,c is_collinear & 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',p are_coplanar & a',b',c',q are_coplanar & a',b',c',r are_coplanar &
not a,b,c,a' are_coplanar implies p,q,r is_collinear;

theorem :: PROJDES1:21
a<>a' & o,a,a' is_collinear & not a,b,c,o are_coplanar & not
a',b',c' is_collinear & a,b,p is_collinear & a',b',p is_collinear &
b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear &
a',c',r is_collinear implies p,q,r is_collinear;

theorem :: PROJDES1:22
not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear
implies not a,b,d,o are_coplanar;

theorem :: PROJDES1:23
not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear
& o,c,c' is_collinear & o<>a' & o<>b' & o<>c' implies
not a',b',c' is_collinear & not a',b',c',o are_coplanar;

theorem :: PROJDES1:24
a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not
a,b,d,o are_coplanar & not b,c,d,o are_coplanar & not a,c,d,o are_coplanar
& o,d,d' is_collinear & o,a,a' is_collinear & o,b,b' is_collinear &
o,c,c' is_collinear & a,d,s is_collinear & a',d',s is_collinear &
b,d,t is_collinear & b',d',t is_collinear & c,d,u is_collinear & o<>a' & o<>d'
& d<>d' & o<>b' implies not s,t,u is_collinear;

definition let FCPS,o,a,b,c;
:: 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;

canceled;

theorem :: PROJDES1:26
not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear
& o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear &
a,b,p is_collinear & a',b',p is_collinear & a<>a' & b,c,r is_collinear &
b',c',r is_collinear & a,c,q is_collinear & b<>b' & a',c',q is_collinear &
o<>a' & o<>b' & o<>c' implies r,q,p is_collinear;

theorem :: PROJDES1:27
for CS being up-3-dimensional CollProjectiveSpace holds
CS is Desarguesian;

definition
cluster -> Desarguesian (up-3-dimensional CollProjectiveSpace);
end;
```