HomeHome Metamath Proof Explorer
Theorem List (p. 356 of 382)
< 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-25961)
  Hilbert Space Explorer  Hilbert Space Explorer
(25962-27486)
  Users' Mathboxes  Users' Mathboxes
(27487-38122)
 

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdalem13 35501 Lemma for dalem14 35502. (Contributed by NM, 21-Jul-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 )   &    |-  W  =  ( Y  .\/  C )   =>    |-  ( ( ph  /\  Y  =/=  Z )  ->  ( Y  .\/  Z )  =  W )
 
Theoremdalem14 35502 Lemma for dath 35561. Planes  Y and 
Z form a 3-dimensional space (when they are different). (Contributed by NM, 22-Jul-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 )   &    |-  V  =  ( LVols `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  W  =  ( Y  .\/  C )   =>    |-  ( ( ph  /\  Y  =/=  Z )  ->  ( Y  .\/  Z )  e.  V )
 
Theoremdalem15 35503 Lemma for dath 35561. The axis of perspectivity  X is a line. (Contributed by NM, 21-Jul-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 )   &    |-  N  =  ( LLines `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  X  =  ( Y  ./\  Z )   =>    |-  ( ( ph  /\  Y  =/=  Z )  ->  X  e.  N )
 
Theoremdalem16 35504 Lemma for dath 35561. The atoms  D,  E, and  F form a line of perspectivity. This is Desargue's Theorem for the special case where planes  Y and  Z are different. (Contributed by NM, 7-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 ) )
 
Theoremdalem17 35505 Lemma for dath 35561. When planes  Y and 
Z are equal, the center of perspectivity  C is in  Y. (Contributed by NM, 1-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  .<_  Y )
 
Theoremdalem18 35506* Lemma for dath 35561. Show that a dummy atom  c exists outside of the  Y and  Z planes (when those planes are equal). This requires that the projective space be 3-dimensional. (Desargue's theorem doesn't always hold in 2 dimensions.) (Contributed by NM, 29-Jul-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 )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   =>    |-  ( ph  ->  E. c  e.  A  -.  c  .<_  Y )
 
Theoremdalem19 35507* Lemma for dath 35561. 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 35508 Lemma for dath 35561. 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 35509 Lemma for dath 35561. 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 35510 Lemma for dath 35561. 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 35511 Lemma for dath 35561. 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 35512 Lemma for dath 35561. 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 35513 Lemma for dath 35561. 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 35514 Lemma for dath 35561. 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 35515 Lemma for dath 35561. 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 35516 Lemma for dath 35561. 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 35517 Lemma for dath 35561. 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 35518* Lemma for dath 35561. 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 35519 Lemma for dath 35561. 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 35520 Lemma for dath 35561. 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 35521 Lemma for dath 35561. 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 35522 Lemma for dath 35561. 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 35523 Lemma for dath 35561. 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 35524 Lemma for dath 35561. 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 35525 Lemma for dath 35561. Lemma dalem27 35524 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 35526 Lemma for dath 35561. Analog of dalem23 35521 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 35527 Lemma for dath 35561. Analog of dalem24 35522 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 35528 Lemma for dath 35561. Analog of dalem25 35523 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 35529 Lemma for dath 35561. Analog of dalem27 35524 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 35530 Lemma for dath 35561. Analog of dalem28 35525 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 35531 Lemma for dath 35561. Analog of dalem23 35521 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 35532 Lemma for dath 35561. Analog of dalem24 35522 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 35533 Lemma for dath 35561. Analog of dalem27 35524 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 35534 Lemma for dath 35561. Analog of dalem28 35525 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 35535 Lemma for dath 35561. 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 35536 Lemma for dath 35561. 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 35537 Lemma for dath 35561. Analog of dalem39 35536 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 35538 Lemma for dath 35561. (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 35539 Lemma for dath 35561. 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 35540 Lemma for dath 35561. 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 35541 Lemma for dath 35561. 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 35542 Lemma for dath 35561. 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 35543 Lemma for dath 35561. Analog of dalem45 35542 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 35544 Lemma for dath 35561. Analog of dalem45 35542 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 35545 Lemma for dath 35561. Analog of dalem45 35542 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 35546 Lemma for dath 35561. Analog of dalem45 35542 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 35547 Lemma for dath 35561. Analog of dalem45 35542 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 35548 Lemma for dath 35561. 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 35549 Lemma for dath 35561. 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 35550 Lemma for dath 35561. The auxliary axis of perspectivity  B is a line (analogous to the actual axis of perspectivity  X in dalem15 35503. (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 35551 Lemma for dath 35561. 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 35552 Lemma for dath 35561. Lines  G H and  P Q intersect at the auxiliary line  B (later shown to be an axis of perspectivity; see dalem60 35557). (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 35553 Lemma for dath 35561. Analog of dalem55 35552 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 35554 Lemma for dath 35561. 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 35555 Lemma for dath 35561. Analog of dalem57 35554 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 35556 Lemma for dath 35561. Analog of dalem57 35554 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 35557 Lemma for dath 35561. 
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 35558 Lemma for dath 35561. 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 35559 Lemma for dath 35561. 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 ) )