HomeHome Metamath Proof Explorer
Theorem List (p. 334 of 357)
< 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-24339)
  Hilbert Space Explorer  Hilbert Space Explorer
(24340-25864)
  Users' Mathboxes  Users' Mathboxes
(25865-35640)
 

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdalemclpjs 33301 Lemma for dath 33403. 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 33302 Lemma for dath 33403. 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 33303 Lemma for dath 33403. 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 33304 Lemma for dath 33403. 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 33305 Lemma for dath 33403. 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 33306 Lemma for dath 33403. 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 33307 Lemma for dath 33403. 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 33308 Lemma for dath 33403. 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 33309 Lemma for dath 33403. 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 33310 Lemma for dath 33403. 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 33311 Lemma for dath 33403. 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 33312 Lemma for dath 33403. 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 33313 Lemma for dath 33403. 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 33314 Lemma for dath 33403. 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 33315 Lemma for dath 33403. 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 33316 Lemma for dath 33403. 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 33317 Lemma for dath 33403. 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 33318 Lemma for dath 33403. 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 33319 Lemma for dath 33403. 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 33320 Lemma for dath 33403. 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 33321 Lemma for dath 33403. 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 33322 Lemma for dath 33403. 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 33323 Lemma for dath 33403. 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 33324 Lemma for dath 33403. 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 33325 Lemma for dath 33403. 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 33326 Lemma for dath 33403. 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 33327 Lemma for dath 33403. 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 33328 Lemma for dath 33403. 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 33329 Lemma for dath 33403. 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 33330 Lemma for dath 33403. 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 33331 Lemma for dalemdnee 33333. (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 33332 Lemma for dalemdnee 33333. (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 33333 Lemma for dath 33403. 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 33334 Lemma for dath 33403. 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 33335 Lemma for dath 33403. Analog of dalem5 33334 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 33336 Lemma for dath 33403. Analog of dalem5 33334 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 33337 Lemma for dath 33403. 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 33338 Lemma for dalem9 33339. 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 33339 Lemma for dath 33403. 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 33340 Lemma for dath 33403. 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 33341 Lemma for dath 33403. Analog of dalem10 33340 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 33342 Lemma for dath 33403. Analog of dalem10 33340 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 33343 Lemma for dalem14 33344. (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 33344 Lemma for dath 33403. 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 33345 Lemma for dath 33403. 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 33346 Lemma for dath 33403. 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 33347 Lemma for dath 33403. 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 33348* Lemma for dath 33403. 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 33349* Lemma for dath 33403. 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 33350 Lemma for dath 33403. 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 33351 Lemma for dath 33403. 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 33352 Lemma for dath 33403. 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 33353 Lemma for dath 33403. 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 33354 Lemma for dath 33403. 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 33355 Lemma for dath 33403. 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 33356 Lemma for dath 33403. 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 33357 Lemma for dath 33403. 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 33358 Lemma for dath 33403. 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 33359 Lemma for dath 33403. 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 33360* Lemma for dath 33403. 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 33361 Lemma for dath 33403. 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 33362 Lemma for dath 33403. 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 33363 Lemma for dath 33403. 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 33364 Lemma for dath 33403. 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 33365 Lemma for dath 33403. 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 33366 Lemma for dath 33403. 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 33367 Lemma for dath 33403. Lemma dalem27 33366 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 33368 Lemma for dath 33403. Analog of dalem23 33363 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 33369 Lemma for dath 33403. Analog of dalem24 33364 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 33370 Lemma for dath 33403. Analog of dalem25 33365 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 33371 Lemma for dath 33403. Analog of dalem27 33366 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 33372 Lemma for dath 33403. Analog of dalem28 33367 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 33373 Lemma for dath 33403. Analog of dalem23 33363 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 33374 Lemma for dath 33403. Analog of dalem24 33364 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 33375 Lemma for dath 33403. Analog of dalem27 33366 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 ) )