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

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-22262)
  Hilbert Space Explorer  Hilbert Space Explorer
(22263-23785)
  Users' Mathboxes  Users' Mathboxes
(23786-32130)
 

Theorem List for Metamath Proof Explorer - 30501-30600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme21j 30501* Combine cdleme20 30489 and cdleme21i 30500 to eliminate  U 
.<_  ( S  .\/  T
) condition. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( 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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  N  =  O )
 
Theoremcdleme21 30502 Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115.  D,  F,  N,  Y,  G,  O represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 30460 and cdleme21j 30501 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( 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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) ) ) 
 ->  N  =  O )
 
Theoremcdleme21k 30503 Eliminate  S  =/=  T condition in cdleme21 30502. (Contributed by NM, 26-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( 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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  ( P  =/=  Q  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P 
 .\/  Q ) ) ) )  ->  N  =  O )
 
Theoremcdleme22aa 30504 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t 
\/ v = p  \/ q implies v = u. (Contributed by NM, 2-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  V  .<_  W  /\  V  .<_  ( P  .\/  Q ) ) )  ->  V  =  U )
 
Theoremcdleme22a 30505 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t 
\/ v = p  \/ q implies v = u. (Contributed by NM, 30-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  T  e.  A )  /\  ( ( V  e.  A  /\  V  .<_  W ) 
 /\  P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q ) ) ) 
 ->  V  =  U )
 
Theoremcdleme22b 30506 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t  \/ v =/= p  \/ q and s  <_ p  \/ q implies  -. t  <_ p  \/ q. (Contributed by NM, 2-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  (
 ( T  .\/  V )  =/=  ( P  .\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) ) 
 ->  -.  T  .<_  ( P 
 .\/  Q ) )
 
Theoremcdleme22cN 30507 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t  \/ v =/= p  \/ q and s  <_ p  \/ q implies  -. v  <_ p  \/ q. (Contributed by NM, 3-Dec-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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 )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( S  .<_  ( T 
 .\/  V )  /\  S  .<_  ( P  .\/  Q ) )  /\  ( T 
 .\/  V )  =/=  ( P  .\/  Q ) ) )  ->  -.  V  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme22d 30508 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) ) )  ->  V  =  ( ( S  .\/  T )  ./\  W ) )
 
Theoremcdleme22e 30509 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. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( 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 ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  ( T  .\/  V )  =  ( P 
 .\/  Q ) )  /\  ( z  e.  A  /\  -.  z  .<_  W ) ) )  ->  N  .<_  ( O  .\/  V ) )
 
Theoremcdleme22eALTN 30510 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. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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 ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  T  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  P  =/=  Q )  /\  ( S  e.  A  /\  ( V  e.  A  /\  V  .<_  W  /\  ( T  .\/  V )  =  ( P  .\/  Q ) )  /\  (
 ( y  e.  A  /\  -.  y  .<_  W ) 
 /\  ( z  e.  A  /\  -.  z  .<_  W ) ) ) )  ->  N  .<_  ( O  .\/  V )
 )
 
Theoremcdleme22f 30511 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 s  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( 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 )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  T  e.  A  /\  ( V  e.  A  /\  V  .<_  W ) ) 
 /\  ( S  =/=  T 
 /\  S  .<_  ( T 
 .\/  V ) ) ) 
 ->  N  .<_  ( F  .\/  V ) )
 
Theoremcdleme22f2 30512 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 30511 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. (Contributed by NM, 7-Dec-2012.)
 |-  .<_  =  ( 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  .\/  ( ( T  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P 
 .\/  Q )  /\  P  =/=  Q ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  F  .<_  ( N  .\/  V )
 )
 
Theoremcdleme22g 30513 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  G represent f(s), f(t) respectively. If s  <_ t  \/ v and  -. s  <_ p  \/ q, then f(s)  <_ f(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( -.  T  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  P  =/=  Q ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  F  .<_  ( G  .\/  V )
 )
 
Theoremcdleme23a 30514 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  V  .<_  W )
 
Theoremcdleme23b 30515 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  V  e.  A )
 
Theoremcdleme23c 30516 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  S  .<_  ( T  .\/  V ) )
 
Theoremcdleme24 30517* Quantified version of cdleme21k 30503. (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 30518* Lemma for cdleme25b 30519. (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 30519* Transform cdleme24 30517. 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 30520* Transform cdleme25b 30519. (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 30521* Transform cdleme25c 30520. (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 30522* Show closure of the unique element in cdleme25c 30520. (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 30523* Change bound variables in cdleme25c 30520. (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 30524* 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 30525* 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 30526* 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 30527* 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 30528* 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 30529* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30527 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 30530* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30527 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 30531* 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 30532* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 30528 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 30533* Lemma for cdleme27N 30534. (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 30534* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme27a 30532. (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 30535* Lemma for cdleme25b 30519. 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 30536* Lemma for cdleme25b 30519. 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 30537* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme28b 30536. 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 30538* Quantified version of cdleme28c 30537. (Compare cdleme24 30517.) (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 30539* Lemma for cdleme29b 30540. (Compare cdleme25a 30518.) 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 30540* Transform cdleme28 30538. (Compare cdleme25b 30519.) 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 30541* Transform cdleme28b 30536. (Compare cdleme25c 30520.) 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 30542* Show closure of the unique element in cdleme28c 30537. (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 30543 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 30544* 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 30545* 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 30546* 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 30547* 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 30548* 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 30549* 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 30550* 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 30551* 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 30552* 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 30553* 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 30554* 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 30555* 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 30556* 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 30557* 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 30558* 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 30559* 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 30560 ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 30195. (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 30561* 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 30562* 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 30563* 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 30564* TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 30563. (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 30565* 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 30195 here and elsewhere, and presence/absence of  s 
.<_  ( P  .\/  Q
) term. Also, why can proof be shortened with cdleme29cl 30542? What is difference from cdlemefs27cl 30578? (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 30566* 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 30567* Lemma for cdlemefs29bpre1N 30582. (Compare cdleme25a 30518.) 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 30568 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 30569* 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 30570* 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 30571* 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 30572* Show closure of the unique element in cdleme29c 30541. 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 30573* 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 30574* 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 30575* 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