HomeHome Metamath Proof Explorer
Theorem List (p. 299 of 322)
< 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-21498)
  Hilbert Space Explorer  Hilbert Space Explorer
(21499-23021)
  Users' Mathboxes  Users' Mathboxes
(23022-32154)
 

Theorem List for Metamath Proof Explorer - 29801-29900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem4atlem12 29801 Lemma for 4at 29802. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( U  e.  A  /\  V  e.  A  /\  W  e.  A )
 )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( ( P  .\/  Q )  .\/  R ) ) )  ->  ( (
 ( P  .\/  Q )  .\/  ( R  .\/  S ) )  .<_  ( ( T  .\/  U )  .\/  ( V  .\/  W ) )  ->  ( ( P  .\/  Q )  .\/  ( R  .\/  S ) )  =  (
 ( T  .\/  U )  .\/  ( V  .\/  W ) ) ) )
 
Theorem4at 29802 Four atoms determine a lattice volume uniquely. Three-dimensional analog of ps-1 29666 and 3at 29679. (Contributed by NM, 11-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( U  e.  A  /\  V  e.  A  /\  W  e.  A )
 )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( ( P  .\/  Q )  .\/  R ) ) )  ->  ( (
 ( P  .\/  Q )  .\/  ( R  .\/  S ) )  .<_  ( ( T  .\/  U )  .\/  ( V  .\/  W ) )  <->  ( ( P 
 .\/  Q )  .\/  ( R  .\/  S ) )  =  ( ( T 
 .\/  U )  .\/  ( V  .\/  W ) ) ) )
 
Theorem4at2 29803 Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( U  e.  A  /\  V  e.  A  /\  W  e.  A )
 )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( ( P  .\/  Q )  .\/  R ) ) )  ->  ( (
 ( ( P  .\/  Q )  .\/  R )  .\/  S )  .<_  ( ( ( T  .\/  U )  .\/  V )  .\/  W )  <->  ( ( ( P  .\/  Q )  .\/  R )  .\/  S )  =  ( (
 ( T  .\/  U )  .\/  V )  .\/  W ) ) )
 
Theoremlplncvrlvol2 29804 A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |-  C  =  (  <o  `  K )   &    |-  P  =  (
 LPlanes `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  P  /\  Y  e.  V ) 
 /\  X  .<_  Y ) 
 ->  X C Y )
 
Theoremlplncvrlvol 29805 An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.)
 |-  B  =  ( Base `  K )   &    |-  C  =  (  <o  `  K )   &    |-  P  =  ( LPlanes `  K )   &    |-  V  =  (
 LVols `  K )   =>    |-  ( ( ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B )  /\  X C Y ) 
 ->  ( X  e.  P  <->  Y  e.  V ) )
 
Theoremlvolcmp 29806 If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  ( ( K  e.  HL  /\  X  e.  V  /\  Y  e.  V ) 
 ->  ( X  .<_  Y  <->  X  =  Y ) )
 
TheoremlvolnltN 29807 Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.)
 |-  .<  =  ( lt `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  ( ( K  e.  HL  /\  X  e.  V  /\  Y  e.  V ) 
 ->  -.  X  .<  Y )
 
Theorem2lplnja 29808 The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 29809 in terms of atoms). (Contributed by NM, 12-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  V )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( S  e.  A  /\  T  e.  A  /\  U  e.  A )  /\  ( S  =/=  T  /\  -.  U  .<_  ( S  .\/  T ) ) )  /\  ( ( ( P 
 .\/  Q )  .\/  R )  .<_  W  /\  (
 ( S  .\/  T )  .\/  U )  .<_  W 
 /\  ( ( P 
 .\/  Q )  .\/  R )  =/=  ( ( S 
 .\/  T )  .\/  U ) ) )  ->  ( ( ( P 
 .\/  Q )  .\/  R )  .\/  ( ( S 
 .\/  T )  .\/  U ) )  =  W )
 
Theorem2lplnj 29809 The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  P  =  (
 LPlanes `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  (
 ( K  e.  HL  /\  ( X  e.  P  /\  Y  e.  P  /\  W  e.  V )  /\  ( X  .<_  W  /\  Y  .<_  W  /\  X  =/=  Y ) )  ->  ( X  .\/  Y )  =  W )
 
Theorem2lplnm2N 29810 The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  N  =  ( LLines `  K )   &    |-  P  =  (
 LPlanes `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  (
 ( K  e.  HL  /\  ( X  e.  P  /\  Y  e.  P  /\  W  e.  V )  /\  ( X  .<_  W  /\  Y  .<_  W  /\  X  =/=  Y ) )  ->  ( X  ./\  Y )  e.  N )
 
Theorem2lplnmj 29811 The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.)
 |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  N  =  ( LLines `  K )   &    |-  P  =  ( LPlanes `  K )   &    |-  V  =  ( LVols `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  P  /\  Y  e.  P )  ->  ( ( X  ./\  Y )  e.  N  <->  ( X  .\/  Y )  e.  V ) )
 
Theoremdalemkehl 29812 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  K  e.  HL )
 
Theoremdalemkelat 29813 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  K  e.  Lat )
 
Theoremdalemkeop 29814 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  K  e.  OP )
 
Theoremdalempea 29815 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  P  e.  A )
 
Theoremdalemqea 29816 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  Q  e.  A )
 
Theoremdalemrea 29817 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  R  e.  A )
 
Theoremdalemsea 29818 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  S  e.  A )
 
Theoremdalemtea 29819 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  T  e.  A )
 
Theoremdalemuea 29820 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  U  e.  A )
 
Theoremdalemyeo 29821 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  Y  e.  O )
 
Theoremdalemzeo 29822 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  Z  e.  O )
 
Theoremdalemclpjs 29823 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  C  .<_  ( P  .\/  S ) )
 
Theoremdalemclqjt 29824 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  C  .<_  ( Q  .\/  T ) )
 
Theoremdalemclrju 29825 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  C  .<_  ( R  .\/  U ) )
 
Theoremdalem-clpjq 29826 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   =>    |-  ( ph  ->  -.  C  .<_  ( P  .\/  Q ) )
 
Theoremdalemceb 29827 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  C  e.  ( Base `  K ) )
 
Theoremdalempeb 29828 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  P  e.  ( Base `  K ) )
 
Theoremdalemqeb 29829 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  Q  e.  ( Base `  K ) )
 
Theoremdalemreb 29830 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  R  e.  ( Base `  K ) )
 
Theoremdalemseb 29831 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  S  e.  ( Base `  K ) )
 
Theoremdalemteb 29832 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  T  e.  ( Base `  K ) )
 
Theoremdalemueb 29833 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ph  ->  U  e.  ( Base `  K ) )
 
Theoremdalempjqeb 29834 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ph  ->  ( P  .\/  Q )  e.  ( Base `  K ) )
 
Theoremdalemsjteb 29835 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ph  ->  ( S  .\/  T )  e.  ( Base `  K ) )
 
Theoremdalemtjueb 29836 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ph  ->  ( T  .\/  U )  e.  ( Base `  K ) )
 
Theoremdalemqrprot 29837 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ph  ->  ( ( Q 
 .\/  R )  .\/  P )  =  ( ( P  .\/  Q )  .\/  R ) )
 
Theoremdalemyeb 29838 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 ) ) ) ) )   &    |-  O  =  (
 LPlanes `  K )   =>    |-  ( ph  ->  Y  e.  ( Base `  K ) )
 
Theoremdalemcnes 29839 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 )   =>    |-  ( ph  ->  C  =/=  S )
 
Theoremdalempnes 29840 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 )   =>    |-  ( ph  ->  P  =/=  S )
 
Theoremdalemqnet 29841 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 )   =>    |-  ( ph  ->  Q  =/=  T )
 
Theoremdalempjsen 29842 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 )   =>    |-  ( ph  ->  ( P  .\/  S )  e.  ( LLines `  K ) )
 
Theoremdalemply 29843 Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-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 )   =>    |-  ( ph  ->  P  .<_  Y )
 
Theoremdalemsly 29844 Lemma for dath 29925. Frequently-used utility lemma. (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 )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ph  /\  Y  =  Z )  ->  S  .<_  Y )
 
Theoremdalemswapyz 29845 Lemma for dath 29925. Swap the role of planes  Y and  Z to allow reuse of analogous proofs. (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 )   =>    |-  ( ph  ->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K ) )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )
 )  /\  ( Z  e.  O  /\  Y  e.  O )  /\  ( ( -.  C  .<_  ( S 
 .\/  T )  /\  -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S ) )  /\  ( -.  C  .<_  ( P  .\/  Q )  /\  -.  C  .<_  ( Q  .\/  R )  /\  -.  C  .<_  ( R  .\/  P )
 )  /\  ( C  .<_  ( S  .\/  P )  /\  C  .<_  ( T 
 .\/  Q )  /\  C  .<_  ( U  .\/  R ) ) ) ) )
 
Theoremdalemrot 29846 Lemma for dath 29925. Rotate triangles  Y  =  P Q R and  Z  =  S T U to allow reuse of analogous proofs. (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 )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  ( ph  ->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K ) )  /\  ( Q  e.  A  /\  R  e.  A  /\  P  e.  A )  /\  ( T  e.  A  /\  U  e.  A  /\  S  e.  A )
 )  /\  ( (
 ( Q  .\/  R )  .\/  P )  e.  O  /\  ( ( T  .\/  U )  .\/  S )  e.  O )  /\  ( ( -.  C  .<_  ( Q  .\/  R )  /\  -.  C  .<_  ( R  .\/  P )  /\  -.  C  .<_  ( P  .\/  Q )
 )  /\  ( -.  C  .<_  ( T  .\/  U )  /\  -.  C  .<_  ( U  .\/  S )  /\  -.  C  .<_  ( S  .\/  T )
 )  /\  ( C  .<_  ( Q  .\/  T )  /\  C  .<_  ( R 
 .\/  U )  /\  C  .<_  ( P  .\/  S ) ) ) ) )
 
Theoremdalemrotyz 29847 Lemma for dath 29925. Rotate triangles  Y  =  P Q R and  Z  =  S T U to allow reuse of analogous proofs. (Contributed by NM, 19-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 )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   =>    |-  (
 ( ph  /\  Y  =  Z )  ->  ( ( Q  .\/  R )  .\/  P )  =  ( ( T  .\/  U )  .\/  S ) )
 
Theoremdalem1 29848 Lemma for dath 29925. Show the lines  P S and  Q T are different. (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 )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   =>    |-  ( ph  ->  ( P  .\/  S )  =/=  ( Q 
 .\/  T ) )
 
Theoremdalemcea 29849 Lemma for dath 29925. Frequently-used utility lemma. Here we show that  C must be an atom. This is an assumption in most presentations of Desargue's theorem; instead, we assume only the  C is a lattice element, in order to make later substitutions for  C easier. (Contributed by NM, 23-Sep-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 )   =>    |-  ( ph  ->  C  e.  A )
 
Theoremdalem2 29850 Lemma for dath 29925. Show the lines  P Q and  S T form a 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 )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   =>    |-  ( ph  ->  ( ( P 
 .\/  Q )  .\/  ( S  .\/  T ) )  e.  O )
 
Theoremdalemdea 29851 Lemma for dath 29925. Frequently-used utility lemma. (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 ) )   =>    |-  ( ph  ->  D  e.  A )
 
Theoremdalemeea 29852 Lemma for dath 29925. Frequently-used utility lemma. (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 )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   =>    |-  ( ph  ->  E  e.  A )
 
Theoremdalem3 29853 Lemma for dalemdnee 29855. (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 )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   =>    |-  ( ( ph  /\  D  =/=  Q ) 
 ->  D  =/=  E )
 
Theoremdalem4 29854 Lemma for dalemdnee 29855. (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 )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   =>    |-  ( ( ph  /\  D  =/=  T ) 
 ->  D  =/=  E )
 
Theoremdalemdnee 29855 Lemma for dath 29925. Axis of perspectivity points  D and  E are different. (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 )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   =>    |-  ( ph  ->  D  =/=  E )
 
Theoremdalem5 29856 Lemma for dath 29925. Atom  U (in plane  Z  =  S T U) belongs to the 3-dimensional volume formed by  Y and 
C. (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 )   &    |-  W  =  ( Y  .\/  C )   =>    |-  ( ph  ->  U  .<_  W )
 
Theoremdalem6 29857 Lemma for dath 29925. Analog of dalem5 29856 for  S. (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  ->  S  .<_  W )
 
Theoremdalem7 29858 Lemma for dath 29925. Analog of dalem5 29856 for  T. (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  ->  T  .<_  W )
 
Theoremdalem8 29859 Lemma for dath 29925. Plane  Z belongs to the 3-dimensional space. (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  ->  Z  .<_  W )
 
Theoremdalem-cly 29860 Lemma for dalem9 29861. Center of perspectivity  C is not in plane  Y (when  Y and  Z are different planes). (Contributed by NM, 13-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 )
 
Theoremdalem9 29861 Lemma for dath 29925. Since  -.  C  .<_  Y, the join  Y  .\/  C forms a 3-dimensional space. (Contributed by NM, 20-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 )  ->  W  e.  V )
 
Theoremdalem10 29862 Lemma for dath 29925. Atom  D belongs to the axis of perspectivity  X. (Contributed by NM, 19-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 )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  X  =  ( Y  ./\  Z )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   =>    |-  ( ph  ->  D  .<_  X )
 
Theoremdalem11 29863 Lemma for dath 29925. Analog of dalem10 29862 for  E. (Contributed by NM, 23-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 )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  X  =  ( Y  ./\  Z )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   =>    |-  ( ph  ->  E  .<_  X )
 
Theoremdalem12 29864 Lemma for dath 29925. Analog of dalem10 29862 for  F. (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 )   &    |-  X  =  ( Y  ./\  Z )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ph  ->  F  .<_  X )
 
Theoremdalem13 29865 Lemma for dalem14 29866. (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 29866 Lemma for dath 29925. 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 29867 Lemma for dath 29925. 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 29868 Lemma for dath 29925. 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 29869 Lemma for dath 29925. 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 29870* Lemma for dath 29925. 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 29871* Lemma for dath 29925. 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 29872 Lemma for dath 29925. 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 29873 Lemma for dath 29925. 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 29874 Lemma for dath 29925. 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 29875 Lemma for dath 29925. 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 29876 Lemma for dath 29925. 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 29877 Lemma for dath 29925. 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 29878 Lemma for dath 29925. 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 29879 Lemma for dath 29925. 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 29880 Lemma for dath 29925. 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 29881 Lemma for dath 29925. 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 29882* Lemma for dath 29925. 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 29883 Lemma for dath 29925. 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 29884 Lemma for dath 29925. 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 29885 Lemma for dath 29925. 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 29886 Lemma for dath 29925. 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 29887 Lemma for dath 29925. 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 )