HomeHome Metamath Proof Explorer
Theorem List (p. 341 of 410)
< 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-26627)
  Hilbert Space Explorer  Hilbert Space Explorer
(26628-28150)
  Users' Mathboxes  Users' Mathboxes
(28151-40909)
 

Theorem List for Metamath Proof Explorer - 34001-34100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme31sn1c 34001* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.)
 |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  C  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   =>    |-  ( ( R  e.  A  /\  R  .<_  ( P  .\/  Q ) )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31sn2 34002* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   &    |-  C  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( R  e.  A  /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31fv 34003* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q  /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  C  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  z  =  ( N  .\/  ( X  ./\  W ) ) ) )   =>    |-  ( X  e.  B  ->  ( F `  X )  =  if (
 ( P  =/=  Q  /\  -.  X  .<_  W ) ,  C ,  X ) )
 
Theoremcdleme31fv1 34004* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q  /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  C  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  z  =  ( N  .\/  ( X  ./\  W ) ) ) )   =>    |-  ( ( X  e.  B  /\  ( P  =/=  Q 
 /\  -.  X  .<_  W ) )  ->  ( F `  X )  =  C )
 
Theoremcdleme31fv1s 34005* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q  /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  ( P  =/=  Q 
 /\  -.  X  .<_  W ) )  ->  ( F `  X )  = 
 [_ X  /  x ]_ O )
 
Theoremcdleme31fv2 34006* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.)
 |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W ) ) 
 ->  ( F `  X )  =  X )
 
Theoremcdleme31id 34007* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.)
 |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  P  =  Q )  ->  ( F `  X )  =  X )
 
Theoremcdlemefrs29pre00 34008 ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 33641. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ps )  /\  s  e.  A )  ->  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R ) 
 <->  ( -.  s  .<_  W 
 /\  ( s  .\/  ( R  ./\  W ) )  =  R ) ) )
 
Theoremcdlemefrs29bpre0 34009* TODO fix comment. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  ( A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s  .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\  W ) ) )  <->  z  =  [_ R  /  s ]_ N ) )
 
Theoremcdlemefrs29bpre1 34010* TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  E. z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) ) )
 
Theoremcdlemefrs29cpre1 34011* TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  E! z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) ) )
 
Theoremcdlemefrs29clN 34012* TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 34011. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( R  ./\ 
 W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  O  e.  B )
 
Theoremcdlemefrs32fva 34013* Part of proof of Lemma E in [Crawley] p. 113. Value of  F at an atom not under  W. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 33641 here and elsewhere, and presence/absence of  s  .<_  ( P 
.\/  Q ) term. Also, why can proof be shortened with cdleme29cl 33990? What is difference from cdlemefs27cl 34026? (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  [_ R  /  x ]_ O  =  [_ R  /  s ]_ N )
 
Theoremcdlemefrs32fva1 34014* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  ( F `  R )  =  [_ R  /  s ]_ N )
 
Theoremcdlemefr29exN 34015* Lemma for cdlemefs29bpre1N 34030. (Compare cdleme25a 33966.) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  A. s  e.  A  C  e.  B )  ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( C  .\/  ( X  ./\  W ) )  e.  B ) )
 
Theoremcdlemefr27cl 34016 Part of proof of Lemma E in [Crawley] p. 113. Closure of  N. (Contributed by NM, 23-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  e.  A  /\  Q  e.  A )  /\  ( s  e.  A  /\  -.  s  .<_  ( P 
 .\/  Q )  /\  P  =/=  Q ) )  ->  N  e.  B )
 
Theoremcdlemefr32sn2aw 34017* Show that  [_ R  / 
s ]_ N is an atom not under  W when  -.  R  .<_  ( P  .\/  Q ). (Contributed by NM, 28-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdlemefr32snb 34018* Show closure of  [_ R  /  s ]_ N. (Contributed by NM, 28-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  s ]_ N  e.  B )
 
Theoremcdlemefr29bpre0N 34019* TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( A. s  e.  A  (
 ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) )  <-> 
 z  =  [_ R  /  s ]_ N ) )
 
Theoremcdlemefr29clN 34020* Show closure of the unique element in cdleme29c 33989. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( R  ./\  W ) )  =  R ) 
 ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  O  e.  B )
 
Theoremcdleme43frv1snN 34021* Value of  [_ R  / 
s ]_ N when  -.  R  .<_  ( P  .\/  Q
). (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   &    |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( R  e.  A  /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  s ]_ N  =  X )
 
Theoremcdlemefr32fvaN 34022* Part of proof of Lemma E in [Crawley] p. 113. Value of  F at an atom not under  W. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  x ]_ O  =  [_ R  /  s ]_ N )
 
Theoremcdlemefr32fva1 34023* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q  /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F `  R )  =  [_ R  /  s ]_ N )
 
Theoremcdlemefr31fv1 34024* Value of  ( F `  R ) when  -.  R  .<_  ( P  .\/  Q
). TODO This may be useful for shortening others that now use riotasv 32577 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q  /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F `  R )  =  X )
 
Theoremcdlemefs29pre00N 34025 FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 33641. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  R  .<_  ( P  .\/  Q ) )  /\  s  e.  A )  ->  (
 ( ( -.  s  .<_  W  /\  s  .<_  ( P  .\/  Q )
 )  /\  ( s  .\/  ( R  ./\  W ) )  =  R )  <-> 
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( R  ./\  W ) )  =  R ) ) )
 
Theoremcdlemefs27cl 34026* Part of proof of Lemma E in [Crawley] p. 113. Closure of  N. TODO FIX COMMENT This is the start of a re-proof of cdleme27cl 33979 etc. with the  s  .<_  ( P 
.\/  Q ) condition (so as to not have the  C hypothesis). (Contributed by NM, 24-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  u  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( s  e.  A  /\  -.  s  .<_  W ) 
 /\  s  .<_  ( P 
 .\/  Q )  /\  P  =/=  Q ) )  ->  N  e.  B )
 
Theoremcdlemefs32sn1aw 34027* Show that  [_ R  / 
s ]_ N is an atom not under  W when  R  .<_  ( P 
.\/  Q ). (Contributed by NM, 24-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  Z  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  R  .<_  ( P  .\/  Q ) )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdlemefs32snb 34028* Show closure of  [_ R  /  s ]_ N. (Contributed by NM, 24-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  [_ R  /  s ]_ N  e.  B )
 
Theoremcdlemefs29bpre0N 34029* TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  ( A. s  e.  A  ( ( ( -.  s  .<_  W  /\  s  .<_  ( P  .\/  Q ) )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) )  <-> 
 z  =  [_ R  /  s ]_ N ) )
 
Theoremcdlemefs29bpre1N 34030* TODO: FIX COMMENT. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  E. z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  s  .<_  ( P  .\/  Q )
 )  /\  ( s  .\/  ( R  ./\  W ) )  =  R ) 
 ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )
 
Theoremcdlemefs29cpre1N 34031* TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  E! z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  s  .<_  ( P  .\/  Q )
 )  /\  ( s  .\/  ( R  ./\  W ) )  =  R ) 
 ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )
 
Theoremcdlemefs29clN 34032* Show closure of the unique element in cdleme29c 33989. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( R  ./\ 
 W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  O  e.  B )
 
Theoremcdleme43fsv1snlem 34033* Value of  [_ R  / 
s ]_ N when  R  .<_  ( P  .\/  Q ). (Contributed by NM, 30-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  Y  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\ 
 W ) ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( R  .\/  S )  ./\ 
 W ) ) )   &    |-  V  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  X  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  V ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P 
 .\/  Q ) ) ) 
 ->  [_ R  /  s ]_ N  =  Z )
 
Theoremcdleme43fsv1sn 34034* Value of  [_ R  / 
s ]_ N when  R  .<_  ( P  .\/  Q ). (Contributed by NM, 30-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  Y  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\ 
 W ) ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( R  .\/  S )  ./\ 
 W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  [_ R  /  s ]_ N  =  Z )
 
Theoremcdlemefs32fvaN 34035* Part of proof of Lemma E in [Crawley] p. 113. Value of  F at an atom not under  W. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 33641 here and elsewhere, and presence/absence of  s  .<_  ( P 
.\/  Q ) term. Also, why can proof be shortened with cdleme27cl 33979? What is difference from cdlemefs27cl 34026? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  [_ R  /  x ]_ O  =  [_ R  /  s ]_ N )
 
Theoremcdlemefs32fva1 34036* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  R  .<_  ( P  .\/  Q ) )  ->  ( F `
  R )  = 
 [_ R  /  s ]_ N )
 
Theoremcdlemefs31fv1 34037* Value of  ( F `  R ) when  R  .<_  ( P  .\/  Q ). TODO This may be useful for shortening others that now use riotasv 32577 3d . TODO: FIX COMMENT. ***END OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW***
       "cdleme3xsn1aw" decreased using "cdlemefs32sn1aw"
       "cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw".
       "cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw".
       "cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw".
       "cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw".
       "cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".
       
(Contributed by NM, 27-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  Y  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  ( F `  R )  =  Z )
 
Theoremcdlemefr44 34038* Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  -.  R  .<_  ( P  .\/  Q ) )  ->  ( F `  R )  = 
 [_ R  /  t ]_ D )
 
Theoremcdlemefs44 34039* Value of fs(r) when r is an atom under pq and s is any atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefs45 34042 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( F `  R )  =  [_ R  /  s ]_ [_ S  /  t ]_ E )
 
Theoremcdlemefr45 34040* Value of f(r) when r is an atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F `  R )  =  [_ R  /  t ]_ D )
 
Theoremcdlemefr45e 34041* Explicit expansion of cdlemefr45 34040. TODO: use to shorten cdlemefr45 34040 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F `  R )  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) ) )
 
Theoremcdlemefs45 34042* Value of fs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  ( F `  R )  = 
 [_ R  /  s ]_ [_ S  /  t ]_ E )
 
Theoremcdlemefs45ee 34043* Explicit expansion of cdlemefs45 34042. TODO: use to shorten cdlemefs45 34042 uses? Should  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
) ) be assigned to a hypothesis letter? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  ( F `  R )  =  ( ( P  .\/  Q )  ./\  ( (
 ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )  .\/  (
 ( R  .\/  S )  ./\  W ) ) ) )
 
Theoremcdlemefs45eN 34044* Explicit expansion of cdlemefs45 34042. TODO: use to shorten cdlemefs45 34042 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  ( F `  R )  =  ( ( P  .\/  Q )  ./\  ( ( F `  S )  .\/  ( ( R  .\/  S )  ./\  W )
 ) ) )
 
Theoremcdleme32sn1awN 34045* Show that  [_ R  / 
s ]_ N is an atom not under  W when  R  .<_  ( P 
.\/  Q ). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  Z  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  R  .<_  ( P  .\/  Q ) )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdleme41sn3a 34046* Show that  [_ R  / 
s ]_ N is under  P  .\/  Q when  R  .<_  ( P 
.\/  Q ). (Contributed by NM, 19-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  Z  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  R  .<_  ( P  .\/  Q ) )  ->  [_ R  /  s ]_ N  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme32sn2awN 34047* Show that  [_ R  / 
s ]_ N is an atom not under  W when  -.  R  .<_  ( P  .\/  Q ). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdleme32snaw 34048* Show that  [_ R  / 
s ]_ N is an atom not under  W. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdleme32snb 34049* Show closure of  [_ R  /  s ]_ N. (Contributed by NM, 1-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  [_ R  /  s ]_ N  e.  B )
 
Theoremcdleme32fva 34050* Part of proof of Lemma D in [Crawley] p. 113. Value of  F at an atom not under  W. (Contributed by NM, 2-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  P  =/=  Q )  ->  [_ R  /  x ]_ O  =  [_ R  /  s ]_ N )
 
Theoremcdleme32fva1 34051* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  P  =/=  Q )  ->  ( F `  R )  =  [_ R  /  s ]_ N )
 
Theoremcdleme32fvaw 34052* Show that  ( F `  R ) is an atom not under  W when  R is an atom not under  W. (Contributed by NM, 18-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  ->  (
 ( F `  R )  e.  A  /\  -.  ( F `  R )  .<_  W ) )
 
Theoremcdleme32fvcl 34053* Part of proof of Lemma D in [Crawley] p. 113. Closure of the function  F. (Contributed by NM, 10-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  X  e.  B )  ->  ( F `  X )  e.  B )
 
Theoremcdleme32a 34054* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  ( P  =/=  Q 
 /\  -.  X  .<_  W ) )  /\  (
 ( s  e.  A  /\  -.  s  .<_  W ) 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( F `  X )  =  ( N  .\/  ( X  ./\ 
 W ) ) )
 
Theoremcdleme32b 34055* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  Y  e.  B  /\  ( P  =/=  Q  /\  -.  X  .<_  W ) )  /\  ( ( s  e.  A  /\  -.  s  .<_  W )  /\  ( s  .\/  ( X 
 ./\  W ) )  =  X  /\  X  .<_  Y ) )  ->  ( F `  Y )  =  ( N  .\/  ( Y  ./\  W ) ) )
 
Theoremcdleme32c 34056* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  Y  e.  B  /\  ( P  =/=  Q  /\  -.  X  .<_  W ) )  /\  ( ( s  e.  A  /\  -.  s  .<_  W )  /\  ( s  .\/  ( X 
 ./\  W ) )  =  X  /\  X  .<_  Y ) )  ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme32d 34057* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  Y  e.  B  /\  ( P  =/=  Q  /\  -.  X  .<_  W ) )  /\  X  .<_  Y )  ->  ( F `  X )  .<_  ( F `
  Y ) )
 
Theoremcdleme32e 34058* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( X  e.  B  /\  Y  e.  B )  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W )  /\  ( P  =/=  Q  /\  -.  Y  .<_  W ) ) 
 /\  ( ( s  e.  A  /\  -.  s  .<_  W )  /\  ( s  .\/  ( Y 
 ./\  W ) )  =  Y  /\  X  .<_  Y ) )  ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme32f 34059* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( X  e.  B  /\  Y  e.  B )  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W )  /\  ( P  =/=  Q  /\  -.  Y  .<_  W ) ) 
 /\  X  .<_  Y ) 
 ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme32le 34060* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  Y  e.  B )  /\  X  .<_  Y ) 
 ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme35a 34061 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F  .\/  U )  =  ( R  .\/  U )
 )
 
Theoremcdleme35fnpq 34062 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL