HomeHome Metamath Proof Explorer
Theorem List (p. 294 of 309)
< 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-21328)
  Hilbert Space Explorer  Hilbert Space Explorer
(21329-22851)
  Users' Mathboxes  Users' Mathboxes
(22852-30843)
 

Theorem List for Metamath Proof Explorer - 29301-29400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemefs32fva1 29301* 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 29302* Value of  ( F `  R ) when  R  .<_  ( P  .\/  Q ). TODO This may be useful for shortening others that now use riotasv 6238 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 29303* 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 29304* 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 29307 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 29305* 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 29306* Explicit expansion of cdlemefr45 29305. TODO: use to shorten cdlemefr45 29305 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 29307* 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 29308* Explicit expansion of cdlemefs45 29307. TODO: use to shorten cdlemefs45 29307 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 29309* Explicit expansion of cdlemefs45 29307. TODO: use to shorten cdlemefs45 29307 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 29310* 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 29311* 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 29312* 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 29313* 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 29314* 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 29315* 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 29316* 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 29317* 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 29318* 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 29319* 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 29320* 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 29321* 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 29322* 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 29323* 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 29324* 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 29325* 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 29326 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 29327 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  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  -.  F  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme35b 29328 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 )
 )  ->  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 )  .<_  ( Q  .\/  ( R  .\/  U ) ) )
 
Theoremcdleme35c 29329 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 )
 )  ->  ( Q  .\/  F )  =  ( Q  .\/  ( ( P  .\/  R )  ./\  W ) ) )
 
Theoremcdleme35d 29330 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 )
 )  ->  ( ( Q  .\/  F )  ./\  W )  =  ( ( P  .\/  R )  ./\ 
 W ) )
 
Theoremcdleme35e 29331 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 )
 )  ->  ( P  .\/  ( ( Q  .\/  F )  ./\  W )
 )  =  ( P 
 .\/  R ) )
 
Theoremcdleme35f 29332 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 )
 )  ->  ( ( R  .\/  U )  ./\  ( P  .\/  R ) )  =  R )
 
Theoremcdleme35g 29333 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 )  ./\  ( P  .\/  ( ( Q  .\/  F )  ./\ 
 W ) ) )  =  R )
 
Theoremcdleme35h 29334 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 11-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 )
 ) )   &    |-  G  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  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  =  G ) )  ->  R  =  S )
 
Theoremcdleme35h2 29335 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 18-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 )
 ) )   &    |-  G  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  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 ) )  ->  F  =/=  G )
 
Theoremcdleme35sn2aw 29336* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line case; compare cdleme32sn2awN 29312. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( 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 ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme35sn3a 29337* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (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 )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( 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 )
 )
 
Theoremcdleme36a 29338 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A )  /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  R  .<_  ( P  .\/  Q )
 )  /\  ( (
 t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) ) )  ->  -.  R  .<_  ( t  .\/  E ) )
 
Theoremcdleme36m 29339 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  C  =  ( ( S  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  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  =  C ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) ) ) ) 
 ->  R  =  S )
 
Theoremcdleme37m 29340 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  C  =  ( ( S  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  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 )
 )  /\  ( (
 t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  C  =  G )
 
Theoremcdleme38m 29341 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  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  =  G ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  R  =  S )
 
Theoremcdleme38n 29342 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT TODO shorter if proved directly from cdleme36m 29339 and cdleme37m 29340? (Contributed by NM, 14-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  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 ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  F  =/=  G )
 
Theoremcdleme39a 29343 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT.  E,  Y,  G,  Z serve as f(t), f(u), ft( R), ft( S). Put hypotheses of cdleme38n 29342 in convention of cdleme32sn1awN 29310. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  P  e.  A  /\  Q  e.  A ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  ( t  e.  A  /\  -.  t  .<_  W ) ) ) 
 ->  G  =  ( ( R  .\/  V )  ./\  ( E  .\/  (
 ( t  .\/  R )  ./\  W ) ) ) )
 
Theoremcdleme39n 29344 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT.  E,  Y,  G,  Z serve as f(t), f(u), ft( R), ft( S). Put hypotheses of cdleme38n 29342 in convention of cdleme32sn1awN 29310. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( S  .\/  u )  ./\  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 ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  G  =/=  Z )
 
Theoremcdleme40m 29345* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 29310. (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  F  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( S  .\/  v )  ./\  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 ) 
 /\  ( v  e.  A  /\  -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) ) ) ) 
 ->  [_ R  /  s ]_ N  =/=  F )
 
Theoremcdleme40n 29346* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  F  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( S  .\/  v )  ./\  W ) ) )   &    |-  X  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  X ) )   &    |-  V  =  if ( u  .<_  ( P  .\/  Q ) ,  O ,  .<  )   &    |-  Z  =  ( iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  F ) )   =>    |-  ( ( ( ( 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 ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  u ]_ V )
 
Theoremcdleme40v 29347* Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in  [_ S  /  u ]_ V (but we use  [_ R  /  u ]_ V for convenience since we have its hypotheses available) . (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   &    |-  D  =  ( (
 s  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  s
 )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  X  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  X ) )   &    |-  V  =  if ( u  .<_  ( P  .\/  Q ) ,  O ,  Y )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ N  =  [_ R  /  u ]_ V )
 
Theoremcdleme40w 29348* Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 29347 bound variable change to  [_ S  /  u ]_ V. TODO: FIX COMMENT (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 )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   &    |-  D  =  ( (
 s  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  s
 )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  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 ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme42a 29349 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  ( R  .\/  S )  =  ( R  .\/  V ) )
 
Theoremcdleme42c 29350 Part of proof of Lemma E in [Crawley] p. 113. Match  -.  x  .<_  W. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  -.  ( R  .\/  V )  .<_  W )
 
Theoremcdleme42d 29351 Part of proof of Lemma E in [Crawley] p. 113. Match  ( s  .\/  ( x  ./\  W
) )  =  x. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  ( R  .\/  (
 ( R  .\/  V )  ./\  W ) )  =  ( R  .\/  V ) )
 
Theoremcdleme41sn3aw 29352* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   =>    |-  ( ( ( ( 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 ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41sn4aw 29353* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off  P  .\/  Q line. TODO: FIX COMMENT (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 )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   =>    |-  ( ( ( ( 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 ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41snaw 29354* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 29313. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   =>    |-  ( ( ( ( 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  =/=  S )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41fva11 29355* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT (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 )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   &    |-  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 )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  R  =/=  S )  ->  ( F `  R )  =/=  ( F `  S ) )
 
Theoremcdleme42b 29356* Part of proof of Lemma E in [Crawley] p. 113. (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 )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   &    |-  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 ) )  /\  (
 ( R  e.  A  /\  -.  R  .<_  W ) 
 /\  ( R  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( F `  X )  =  (
 [_ R  /  s ]_ N  .\/  ( X 
 ./\  W ) ) )
 
Theoremcdleme42e 29357* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  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 )   &    |-  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 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  ( R  .\/  V ) )  =  ( [_ R  /  s ]_ N  .\/  ( ( R  .\/  V )  ./\ 
 W ) ) )
 
Theoremcdleme42f 29358* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )