HomeHome Metamath Proof Explorer
Theorem List (p. 341 of 357)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-24325)
  Hilbert Space Explorer  Hilbert Space Explorer
(24326-25850)
  Users' Mathboxes  Users' Mathboxes
(25851-35622)
 

Theorem List for Metamath Proof Explorer - 34001-34100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme24 34001* Quantified version of cdleme21k 33987. (Contributed by NM, 26-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  G  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( R  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  A. s  e.  A  A. t  e.  A  ( ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) ) )  ->  N  =  O )
 )
 
Theoremcdleme25a 34002* Lemma for cdleme25b 34003. (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  N  e.  B ) )
 
Theoremcdleme25b 34003* Transform cdleme24 34001. TODO get rid of $d's on  U,  N (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E. u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )
 
Theoremcdleme25c 34004* Transform cdleme25b 34003. (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E! u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )
 
Theoremcdleme25dN 34005* Transform cdleme25c 34004. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E! u  e.  B  E. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  u  =  N ) )
 
Theoremcdleme25cl 34006* Show closure of the unique element in cdleme25c 34004. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  I  e.  B )
 
Theoremcdleme25cv 34007* Change bound variables in cdleme25c 34004. (Contributed by NM, 2-Feb-2013.)
 |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  G  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( R  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  I  =  E
 
Theoremcdleme26e 34008* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P  .\/  Q )
 )  /\  ( ( T  .\/  V )  =  ( P  .\/  Q )  /\  -.  z  .<_  ( P  .\/  Q )
 )  /\  ( z  e.  A  /\  -.  z  .<_  W ) ) ) 
 ->  I  .<_  ( E 
 .\/  V ) )
 
Theoremcdleme26ee 34009* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P  .\/  Q )
 )  /\  ( T  .\/  V )  =  ( P  .\/  Q )
 ) )  ->  I  .<_  ( E  .\/  V ) )
 
Theoremcdleme26eALTN 34010* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( y  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  y )  ./\  W ) ) )   &    |-  G  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  y )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. y  e.  A  ( ( -.  y  .<_  W 
 /\  -.  y  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( S  e.  A  /\  -.  S  .<_  W 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( T  e.  A  /\  -.  T  .<_  W  /\  T  .<_  ( P  .\/  Q ) ) )  /\  ( ( V  e.  A  /\  V  .<_  W  /\  ( T  .\/  V )  =  ( P  .\/  Q ) )  /\  (
 y  e.  A  /\  -.  y  .<_  W  /\  -.  y  .<_  ( P  .\/  Q ) )  /\  (
 z  e.  A  /\  -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) ) ) ) 
 ->  I  .<_  ( E 
 .\/  V ) )
 
Theoremcdleme26fALTN 34011* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  N represent f(t), ft(s) respectively. If t  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  (
 ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  /\  ( S  =/=  t  /\  S  .<_  ( t  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  I  .<_  ( F  .\/  V ) )
 
Theoremcdleme26f 34012* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  N represent f(t), ft(s) respectively. If t  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  t  .<_  ( P 
 .\/  Q )  /\  ( S  =/=  t  /\  S  .<_  ( t  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) ) 
 ->  I  .<_  ( F 
 .\/  V ) )
 
Theoremcdleme26f2ALTN 34013* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 34011 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  G  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  s )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  T  .<_  ( P 
 .\/  Q ) )  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  /\  ( s  =/=  T  /\  s  .<_  ( T  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  G  .<_  ( E  .\/  V ) )
 
Theoremcdleme26f2 34014* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 34011 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  G  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  s )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  T  .<_  ( P 
 .\/  Q ) )  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  ( -.  s  .<_  ( P 
 .\/  Q )  /\  (
 s  =/=  T  /\  s  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  G  .<_  ( E  .\/  V )
 )
 
Theoremcdleme27cl 34015* Part of proof of Lemma E in [Crawley] p. 113. Closure of  C. (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( s  e.  A  /\  -.  s  .<_  W ) 
 /\  P  =/=  Q ) )  ->  C  e.  B )
 
Theoremcdleme27a 34016* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 34012 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  =/=  Q  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( s  =/=  t  /\  s  .<_  ( t  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  C  .<_  ( Y  .\/  V ) )
 
Theoremcdleme27b 34017* Lemma for cdleme27N 34018. (Contributed by NM, 3-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( s  =  t  ->  C  =  Y )
 
Theoremcdleme27N 34018* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme27a 34016. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  =/=  Q  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  .<_  ( t 
 .\/  V )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  C  .<_  ( Y  .\/  V )
 )
 
Theoremcdleme28a 34019* Lemma for cdleme25b 34003. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   &    |-  V  =  ( (
 s  .\/  t )  ./\  ( X  ./\  W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  =/=  t  /\  (
 ( s  .\/  ( X  ./\  W ) )  =  X  /\  (
 t  .\/  ( X  ./\ 
 W ) )  =  X )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  .<_  ( Y  .\/  ( X  ./\  W ) ) )
 
Theoremcdleme28b 34020* Lemma for cdleme25b 34003. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  =/=  t  /\  (
 ( s  .\/  ( X  ./\  W ) )  =  X  /\  (
 t  .\/  ( X  ./\ 
 W ) )  =  X )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  =  ( Y 
 .\/  ( X  ./\  W ) ) )
 
Theoremcdleme28c 34021* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme28b 34020. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( s  .\/  ( X  ./\ 
 W ) )  =  X  /\  ( t 
 .\/  ( X  ./\  W ) )  =  X  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  =  ( Y  .\/  ( X  ./\ 
 W ) ) )
 
Theoremcdleme28 34022* Quantified version of cdleme28c 34021. (Compare cdleme24 34001.) (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( 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  A. t  e.  A  ( ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( -.  t  .<_  W  /\  ( t 
 .\/  ( X  ./\  W ) )  =  X ) )  ->  ( C 
 .\/  ( X  ./\  W ) )  =  ( Y  .\/  ( X  ./\ 
 W ) ) ) )
 
Theoremcdleme29ex 34023* Lemma for cdleme29b 34024. (Compare cdleme25a 34002.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( C  .\/  ( X  ./\  W ) )  e.  B ) )
 
Theoremcdleme29b 34024* Transform cdleme28 34022. (Compare cdleme25b 34003.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E. v  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )
 
Theoremcdleme29c 34025* Transform cdleme28b 34020. (Compare cdleme25c 34004.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E! v  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )
 
Theoremcdleme29cl 34026* Show closure of the unique element in cdleme28c 34021. (Contributed by NM, 8-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B  A. z  e.  A  ( ( -.  z  .<_  W 
 /\  -.  z  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  I  =  ( iota_ v  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( X  ./\ 
 W ) )  =  X )  ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  I  e.  B )
 
Theoremcdleme30a 34027 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  A  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  Y  e.  B )  /\  ( ( s  .\/  ( X  ./\  W ) )  =  X  /\  X  .<_  Y ) ) 
 ->  ( s  .\/  ( Y  ./\  W ) )  =  Y )
 
Theoremcdleme31so 34028* 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 ) ) ) )   &    |-  C  =  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( X  ./\ 
 W ) )  =  X )  ->  z  =  ( N  .\/  ( X  ./\  W ) ) ) )   =>    |-  ( X  e.  B  -> 
 [_ X  /  x ]_ O  =  C )
 
Theoremcdleme31sn 34029* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  C  =  if ( R  .<_  ( P  .\/  Q ) ,  [_ R  /  s ]_ I ,  [_ R  /  s ]_ D )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31sn1 34030* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  I  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  C  =  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  [_ R  /  s ]_ G ) )   =>    |-  ( ( R  e.  A  /\  R  .<_  ( P  .\/  Q ) )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31se 34031* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  T )  ./\  W )
 ) )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  T )  ./\  W )
 ) )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ E  =  Y )
 
Theoremcdleme31se2 34032* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.)
 |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( [_ S  /  t ]_ D  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( S  e.  A  -> 
 [_ S  /  t ]_ E  =  Y )
 
Theoremcdleme31sc 34033* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
 |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ C  =  X )
 
Theoremcdleme31sde 34034* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
 |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( R  e.  A  /\  S  e.  A )  ->  [_ R  /  s ]_ [_ S  /  t ]_ E  =  Z )
 
Theoremcdleme31snd 34035* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.)
 |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( v  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  v )  ./\  W ) ) )   &    |-  E  =  ( ( O  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  O )  ./\  W )
 ) )   &    |-  O  =  ( ( S  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   =>    |-  ( S  e.  A  -> 
 [_ S  /  v ]_ [_ N  /  t ]_ D  =  E )
 
Theoremcdleme31sdnN 34036* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.)
 |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  N  =  if (
 s  .<_  ( P  .\/  Q ) ,  I ,  [_ s  /  t ]_ D )
 
Theoremcdleme31sn1c 34037* 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 34038* 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 34039* 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 34040* 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 34041* 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 34042* 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 34043* 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 34044 ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 33679. (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 34045* 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 34046* 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 34047* 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 34048* TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 34047. (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 34049* 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 33679 here and elsewhere, and presence/absence of  s 
.<_  ( P  .\/  Q
) term. Also, why can proof be shortened with cdleme29cl 34026? What is difference from cdlemefs27cl 34062? (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 34050* 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 34051* Lemma for cdlemefs29bpre1N 34066. (Compare cdleme25a 34002.) 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 34052 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 34053* 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 34054* 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 34055* 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 34056* Show closure of the unique element in cdleme29c 34025. 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 34057* 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 34058* 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 34059* 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 34060* Value of  ( F `  R ) when  -.  R  .<_  ( P  .\/  Q
). TODO This may be useful for shortening others that now use riotasv 32615 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 34061 FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 33679. (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 34062* 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 34015 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 34063* 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 34064* 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 34065* 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 34066* 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 34067* 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 34068* Show closure of the unique element in cdleme29c 34025. (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 34069* 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 34070* 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 )