HomeHome Metamath Proof Explorer
Theorem List (p. 291 of 313)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21423)
  Hilbert Space Explorer  Hilbert Space Explorer
(21424-22946)
  Users' Mathboxes  Users' Mathboxes
(22947-31284)
 

Theorem List for Metamath Proof Explorer - 29001-29100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdalem19 29001* Lemma for dath 29055. Show that a second dummy atom  d exists outside of the  Y and  Z planes (when those planes are equal). (Contributed by NM, 15-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ( ( ph  /\  Y  =  Z ) 
 /\  c  e.  A )  /\  -.  c  .<_  Y )  ->  E. d  e.  A  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d )
 ) )
 
Theoremdalemccea 29002 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  c  e.  A )
 
Theoremdalemddea 29003 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  d  e.  A )
 
Theoremdalem-ccly 29004 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  -.  c  .<_  Y )
 
Theoremdalem-ddly 29005 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  -.  d  .<_  Y )
 
Theoremdalemccnedd 29006 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  c  =/=  d )
 
Theoremdalemclccjdd 29007 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ps  ->  C  .<_  ( c  .\/  d )
 )
 
Theoremdalemcceb 29008 Lemma for dath 29055. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
 |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ps  ->  c  e.  ( Base `  K )
 )
 
Theoremdalemswapyzps 29009 Lemma for dath 29055. Swap the  Y and 
Z planes, along with dummy concurrency (center of perspectivity) atoms  c and  d, to allow reuse of analogous proofs. (Contributed by NM, 17-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( d  e.  A  /\  c  e.  A )  /\  -.  d  .<_  Z  /\  (
 c  =/=  d  /\  -.  c  .<_  Z  /\  C  .<_  ( d  .\/  c
 ) ) ) )
 
Theoremdalemrotps 29010 Lemma for dath 29055. Rotate triangles  Y  =  P Q R and  Z  =  S T U to allow reuse of analogous proofs. (Contributed by NM, 15-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   =>    |-  ( ( ph  /\  ps )  ->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  ( ( Q 
 .\/  R )  .\/  P )  /\  ( d  =/=  c  /\  -.  d  .<_  ( ( Q  .\/  R )  .\/  P )  /\  C  .<_  ( c  .\/  d ) ) ) )
 
Theoremdalemcjden 29011 Lemma for dath 29055. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   =>    |-  ( ( ph  /\  ps )  ->  ( c  .\/  d )  e.  ( LLines `
  K ) )
 
Theoremdalem20 29012* Lemma for dath 29055. Show that a second dummy atom  d exists outside of the  Y and  Z planes (when those planes are equal). (Contributed by NM, 14-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ph  /\  Y  =  Z )  ->  E. c E. d ps )
 
Theoremdalem21 29013 Lemma for dath 29055. Show that lines  c d and  P S intersect at an atom. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( c  .\/  d )  ./\  ( P 
 .\/  S ) )  e.  A )
 
Theoremdalem22 29014 Lemma for dath 29055. Show that lines  c d and  P S determine a plane. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( c  .\/  d )  .\/  ( P 
 .\/  S ) )  e.  O )
 
Theoremdalem23 29015 Lemma for dath 29055. Show that auxiliary atom  G is an atom. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  G  e.  A )
 
Theoremdalem24 29016 Lemma for dath 29055. Show that auxiliary atom  G is outside of plane  Y. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  G  .<_  Y )
 
Theoremdalem25 29017 Lemma for dath 29055. Show that the dummy center of perspectivity  c is different from auxiliary atom  G. (Contributed by NM, 3-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  =/=  G )
 
Theoremdalem27 29018 Lemma for dath 29055. Show that the line  G P intersects the dummy center of perspectivity  c. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  .<_  ( G  .\/  P )
 )
 
Theoremdalem28 29019 Lemma for dath 29055. Lemma dalem27 29018 expressed differently. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  P  .<_  ( G  .\/  c )
 )
 
Theoremdalem29 29020 Lemma for dath 29055. Analog of dalem23 29015 for  H. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  H  e.  A )
 
Theoremdalem30 29021 Lemma for dath 29055. Analog of dalem24 29016 for  H. (Contributed by NM, 3-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  H  .<_  Y )
 
Theoremdalem31N 29022 Lemma for dath 29055. Analog of dalem25 29017 for  H. (Contributed by NM, 4-Aug-2012.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  =/=  H )
 
Theoremdalem32 29023 Lemma for dath 29055. Analog of dalem27 29018 for  H. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  .<_  ( H  .\/  Q )
 )
 
Theoremdalem33 29024 Lemma for dath 29055. Analog of dalem28 29019 for  H. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  Q  .<_  ( H  .\/  c )
 )
 
Theoremdalem34 29025 Lemma for dath 29055. Analog of dalem23 29015 for  I. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  I  e.  A )
 
Theoremdalem35 29026 Lemma for dath 29055. Analog of dalem24 29016 for  I. (Contributed by NM, 3-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  I  .<_  Y )
 
Theoremdalem36 29027 Lemma for dath 29055. Analog of dalem27 29018 for  I. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  .<_  ( I  .\/  R )
 )
 
Theoremdalem37 29028 Lemma for dath 29055. Analog of dalem28 29019 for  I. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  R  .<_  ( I  .\/  c )
 )
 
Theoremdalem38 29029 Lemma for dath 29055. Plane  Y belongs to the 3-dimensional volume  G H I c. (Contributed by NM, 5-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  Y  .<_  ( ( ( G  .\/  H )  .\/  I )  .\/  c ) )
 
Theoremdalem39 29030 Lemma for dath 29055. Auxiliary atoms  G,  H, and  I are not colinear. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  H  .<_  ( I  .\/  G )
 )
 
Theoremdalem40 29031 Lemma for dath 29055. Analog of dalem39 29030 for  I. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  I  .<_  ( G  .\/  H )
 )
 
Theoremdalem41 29032 Lemma for dath 29055. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  G  =/=  H )
 
Theoremdalem42 29033 Lemma for dath 29055. Auxiliary atoms  G H I form a plane. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  .\/  I )  e.  O )
 
Theoremdalem43 29034 Lemma for dath 29055. Planes  G H I and  Y are different. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  .\/  I )  =/=  Y )
 
Theoremdalem44 29035 Lemma for dath 29055. Dummy center of perspectivity  c lies outside of plane  G H I. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( ( G  .\/  H )  .\/  I )
 )
 
Theoremdalem45 29036 Lemma for dath 29055. Dummy center of perspectivity  c is not on the line  G H. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( G  .\/  H ) )
 
Theoremdalem46 29037 Lemma for dath 29055. Analog of dalem45 29036 for  H I. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( H  .\/  I
 ) )
 
Theoremdalem47 29038 Lemma for dath 29055. Analog of dalem45 29036 for  I G. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( I  .\/  G ) )
 
Theoremdalem48 29039 Lemma for dath 29055. Analog of dalem45 29036 for  P Q. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( P  .\/  Q ) )
 
Theoremdalem49 29040 Lemma for dath 29055. Analog of dalem45 29036 for  Q R. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( Q  .\/  R ) )
 
Theoremdalem50 29041 Lemma for dath 29055. Analog of dalem45 29036 for  R P. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( R  .\/  P ) )
 
Theoremdalem51 29042 Lemma for dath 29055. Construct the condition  ph with  c,  G H I, and 
Y in place of  C,  Y, and  Z respectively. This lets us reuse the special case of Desargues' Theorem where  Y  =/=  Z, to eventually prove the case where  Y  =  Z. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( (
 ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) )  /\  ( ( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  ( ( -.  c  .<_  ( G 
 .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P )
 )  /\  ( c  .<_  ( G  .\/  P )  /\  c  .<_  ( H 
 .\/  Q )  /\  c  .<_  ( I  .\/  R ) ) ) ) 
 /\  ( ( G 
 .\/  H )  .\/  I
 )  =/=  Y )
 )
 
Theoremdalem52 29043 Lemma for dath 29055. Lines  G H and  P Q intersect at an atom. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  A )
 
Theoremdalem53 29044 Lemma for dath 29055. The auxliary axis of perspectivity  B is a line (analogous to the actual axis of perspectivity  X in dalem15 28997. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  N  =  ( LLines `  K )   &    |-  O  =  (
 LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  B  e.  N )
 
Theoremdalem54 29045 Lemma for dath 29055. Line  G H intersects the auxiliary axis of perspectivity  B. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  B )  e.  A )
 
Theoremdalem55 29046 Lemma for dath 29055. Lines  G H and  P Q intersect at the auxiliary line  B (later shown to be an axis of perspectivity; see dalem60 29051). (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  =  ( ( G  .\/  H )  ./\ 
 B ) )
 
Theoremdalem56 29047 Lemma for dath 29055. Analog of dalem55 29046 for line  S T. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( S  .\/  T ) )  =  ( ( G  .\/  H )  ./\ 
 B ) )
 
Theoremdalem57 29048 Lemma for dath 29055. Axis of perspectivity point  D is on the auxiliary line  B. (Contributed by NM, 9-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  D  .<_  B )
 
Theoremdalem58 29049 Lemma for dath 29055. Analog of dalem57 29048 for  E. (Contributed by NM, 10-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  E  .<_  B )
 
Theoremdalem59 29050 Lemma for dath 29055. Analog of dalem57 29048 for  F. (Contributed by NM, 10-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  F  .<_  B )
 
Theoremdalem60 29051 Lemma for dath 29055. 
B is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( D  .\/  E )  =  B )
 
Theoremdalem61 29052 Lemma for dath 29055. Show that atoms  D,  E, and  F lie on the same line (axis of perspectivity). Eliminate hypotheses containing dummy atoms  c and  d. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  F  .<_  ( D  .\/  E )
 )
 
Theoremdalem62 29053 Lemma for dath 29055. Eliminate the condition  ps containing dummy variables  c and  d. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z ) 
 ->  F  .<_  ( D  .\/  E ) )
 
Theoremdalem63 29054 Lemma for dath 29055. Combine the cases where  Y and  Z are different planes with the case where  Y and 
Z are the same plane. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K )
 )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  (
 ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q 
 .\/  R )  /\  -.  C  .<_  ( R  .\/  P ) )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ph  ->  F 
 .<_  ( D  .\/  E ) )
 
Theoremdath 29055 Desargues' Theorem of projective geometry (proved for a Hilbert lattice). Assume each triple of atoms (points)  P Q R and  S T U forms a triangle (i.e. determines a plane). Assume that lines  P S,  Q T, and  R U meet at a "center of perspectivity"  C. (We also assume that  C is not on any of the 6 lines forming the two triangles.) Then the atoms 
D  =  ( P 
.\/  Q )  ./\  ( S  .\/  T ),  E  =  ( Q  .\/  R ) 
./\  ( T  .\/  U ),  F  =  ( R  .\/  P ) 
./\  ( U  .\/  S ) are colinear, forming an "axis of perspectivity".

Our proof roughly follows Theorem 2.7.1, p. 78 in Beutelspacher and Rosenbaum, Projective Geometry: From Foundations to Applications, Cambridge University Press (1988). Unlike them, we don't assume  C is an atom to make this theorem slightly more general for easier future use. However, we prove that 
C must be an atom in dalemcea 28979.

For a visual demonstration, see the "Desargue's Theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html. The points I, J, and K there define the axis of perspectivity.

See theorem dalaw 29205 for Desargues Law, which eliminates all of the preconditions on the atoms except for central perspectivity. (Contributed by NM, 20-Aug-2012.)

 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ( ( K  e.  HL  /\  C  e.  B ) 
 /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) 
 /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( ( ( P  .\/  Q )  .\/  R )  e.  O  /\  ( ( S  .\/  T )  .\/  U )  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q  .\/  R )  /\  -.  C  .<_  ( R  .\/  P )
 )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) 
 ->  F  .<_  ( D  .\/  E ) )
 
Theoremdath2 29056 Version of Desargues' Theorem dath 29055 with a different variable ordering. (Contributed by NM, 7-Oct-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ( ( K  e.  HL  /\  C  e.  B ) 
 /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) 
 /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A ) )  /\  ( ( ( P  .\/  Q )  .\/  R )  e.  O  /\  ( ( S  .\/  T )  .\/  U )  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q  .\/  R )  /\  -.  C  .<_  ( R  .\/  P )
 )  /\  ( -.  C  .<_  ( S  .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )
 )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
 .\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) 
 ->  D  .<_  ( E  .\/  F ) )
 
Theoremlineset 29057* The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  ( K  e.  B  ->  N  =  { s  | 
 E. q  e.  A  E. r  e.  A  ( q  =/=  r  /\  s  =  { p  e.  A  |  p  .<_  ( q  .\/  r ) } ) } )
 
Theoremisline 29058* The predicate "is a line". (Contributed by NM, 19-Sep-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  N  <->  E. q  e.  A  E. r  e.  A  ( q  =/=  r  /\  X  =  { p  e.  A  |  p  .<_  ( q  .\/  r ) } ) ) )
 
Theoremislinei 29059* Condition implying "is a line". (Contributed by NM, 3-Feb-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  (
 ( ( K  e.  D  /\  Q  e.  A  /\  R  e.  A ) 
 /\  ( Q  =/=  R 
 /\  X  =  { p  e.  A  |  p  .<_  ( Q  .\/  R ) } ) ) 
 ->  X  e.  N )
 
TheorempointsetN 29060* The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  ( K  e.  B  ->  P  =  { p  |  E. a  e.  A  p  =  { a } } )
 
TheoremispointN 29061* The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  P  <->  E. a  e.  A  X  =  { a } ) )
 
TheorematpointN 29062 The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  (
 ( K  e.  D  /\  X  e.  A ) 
 ->  { X }  e.  P )
 
Theorempsubspset 29063* The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  B  ->  S  =  { s  |  ( s  C_  A  /\  A. p  e.  s  A. q  e.  s  A. r  e.  A  ( r  .<_  ( p 
 .\/  q )  ->  r  e.  s )
 ) } )
 
Theoremispsubsp 29064* The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  S  <->  ( X  C_  A  /\  A. p  e.  X  A. q  e.  X  A. r  e.  A  ( r  .<_