HomeHome Metamath Proof Explorer
Theorem List (p. 300 of 315)
< 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-21490)
  Hilbert Space Explorer  Hilbert Space Explorer
(21491-23013)
  Users' Mathboxes  Users' Mathboxes
(23014-31421)
 

Theorem List for Metamath Proof Explorer - 29901-30000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme32e 29901* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( X  e.  B  /\  Y  e.  B )  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W )  /\  ( P  =/=  Q  /\  -.  Y  .<_  W ) ) 
 /\  ( ( s  e.  A  /\  -.  s  .<_  W )  /\  ( s  .\/  ( Y 
 ./\  W ) )  =  Y  /\  X  .<_  Y ) )  ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme32f 29902* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( X  e.  B  /\  Y  e.  B )  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W )  /\  ( P  =/=  Q  /\  -.  Y  .<_  W ) ) 
 /\  X  .<_  Y ) 
 ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme32le 29903* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  C )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  Y  e.  B )  /\  X  .<_  Y ) 
 ->  ( F `  X )  .<_  ( F `  Y ) )
 
Theoremcdleme35a 29904 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( F  .\/  U )  =  ( R  .\/  U )
 )
 
Theoremcdleme35fnpq 29905 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  -.  F  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme35b 29906 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 )  .<_  ( Q  .\/  ( R  .\/  U ) ) )
 
Theoremcdleme35c 29907 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( Q  .\/  F )  =  ( Q  .\/  ( ( P  .\/  R )  ./\  W ) ) )
 
Theoremcdleme35d 29908 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( ( Q  .\/  F )  ./\  W )  =  ( ( P  .\/  R )  ./\ 
 W ) )
 
Theoremcdleme35e 29909 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( P  .\/  ( ( Q  .\/  F )  ./\  W )
 )  =  ( P 
 .\/  R ) )
 
Theoremcdleme35f 29910 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( ( R  .\/  U )  ./\  ( P  .\/  R ) )  =  R )
 
Theoremcdleme35g 29911 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( ( F  .\/  U )  ./\  ( P  .\/  ( ( Q  .\/  F )  ./\ 
 W ) ) )  =  R )
 
Theoremcdleme35h 29912 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  F  =  G ) )  ->  R  =  S )
 
Theoremcdleme35h2 29913 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) )  ->  F  =/=  G )
 
Theoremcdleme35sn2aw 29914* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of  P  .\/  Q line case; compare cdleme32sn2awN 29890. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme35sn3a 29915* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  -.  [_ R  /  s ]_ N  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme36a 29916 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A )  /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  R  .<_  ( P  .\/  Q )
 )  /\  ( (
 t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) ) )  ->  -.  R  .<_  ( t  .\/  E ) )
 
Theoremcdleme36m 29917 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  C  =  ( ( S  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  F  =  C ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) ) ) ) 
 ->  R  =  S )
 
Theoremcdleme37m 29918 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  C  =  ( ( S  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )
 )  /\  ( (
 t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  C  =  G )
 
Theoremcdleme38m 29919 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  F  =  G ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  R  =  S )
 
Theoremcdleme38n 29920 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT TODO shorter if proved directly from cdleme36m 29917 and cdleme37m 29918? (Contributed by NM, 14-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  D  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   &    |-  X  =  ( ( u  .\/  D )  ./\  W )   &    |-  F  =  ( ( R  .\/  V )  ./\  ( E  .\/  ( ( t  .\/  R )  ./\  W )
 ) )   &    |-  G  =  ( ( S  .\/  X )  ./\  ( D  .\/  ( ( u  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  F  =/=  G )
 
Theoremcdleme39a 29921 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT.  E,  Y,  G,  Z serve as f(t), f(u), ft( R), ft( S). Put hypotheses of cdleme38n 29920 in convention of cdleme32sn1awN 29888. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  V  =  ( ( t  .\/  E )  ./\  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  P  e.  A  /\  Q  e.  A ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  ( t  e.  A  /\  -.  t  .<_  W ) ) ) 
 ->  G  =  ( ( R  .\/  V )  ./\  ( E  .\/  (
 ( t  .\/  R )  ./\  W ) ) ) )
 
Theoremcdleme39n 29922 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT.  E,  Y,  G,  Z serve as f(t), f(u), ft( R), ft( S). Put hypotheses of cdleme38n 29920 in convention of cdleme32sn1awN 29888. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( S  .\/  u )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) 
 /\  ( ( t  e.  A  /\  -.  t  .<_  W )  /\  -.  t  .<_  ( P  .\/  Q ) )  /\  (
 ( u  e.  A  /\  -.  u  .<_  W ) 
 /\  -.  u  .<_  ( P  .\/  Q )
 ) ) )  ->  G  =/=  Z )
 
Theoremcdleme40m 29923* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 29888. (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  C  =  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  F  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( S  .\/  v )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) 
 /\  ( v  e.  A  /\  -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) ) ) ) 
 ->  [_ R  /  s ]_ N  =/=  F )
 
Theoremcdleme40n 29924* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on  P  .\/  Q line. TODO: FIX COMMENT TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  C  =  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  F  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( S  .\/  v )  ./\  W ) ) )   &    |-  X  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  X ) )   &    |-  V  =  if ( u  .<_  ( P  .\/  Q ) ,  O ,  .<  )   &    |-  Z  =  ( iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  F ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  u ]_ V )
 
Theoremcdleme40v 29925* Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in  [_ S  /  u ]_ V (but we use  [_ R  /  u ]_ V for convenience since we have its hypotheses available) . (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  D  =  ( (
 s  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  s
 )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   &    |-  T  =  ( ( v  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  v )  ./\  W ) ) )   &    |-  X  =  ( ( P  .\/  Q )  ./\  ( T  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  O  =  (
 iota_ z  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( P  .\/  Q ) )  ->  z  =  X ) )   &    |-  V  =  if ( u  .<_  ( P  .\/  Q ) ,  O ,  Y )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ N  =  [_ R  /  u ]_ V )
 
Theoremcdleme40w 29926* Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 29925 bound variable change to  [_ S  /  u ]_ V. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  D  =  ( (
 s  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  s
 )  ./\  W ) ) )   &    |-  Y  =  ( ( u  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  u )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  S  .<_  ( P 
 .\/  Q )  /\  R  =/=  S ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme42a 29927 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  ( R  .\/  S )  =  ( R  .\/  V ) )
 
Theoremcdleme42c 29928 Part of proof of Lemma E in [Crawley] p. 113. Match  -.  x  .<_  W. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  -.  ( R  .\/  V )  .<_  W )
 
Theoremcdleme42d 29929 Part of proof of Lemma E in [Crawley] p. 113. Match  ( s  .\/  ( x  ./\  W
) )  =  x. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 ->  ( R  .\/  (
 ( R  .\/  V )  ./\  W ) )  =  ( R  .\/  V ) )
 
Theoremcdleme41sn3aw 29930* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41sn4aw 29931* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off  P  .\/  Q line. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  R  .<_  ( P  .\/  Q )  /\  S  .<_  ( P  .\/  Q )  /\  R  =/=  S ) )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41snaw 29932* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 29891. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  R  =/=  S )  ->  [_ R  /  s ]_ N  =/=  [_ S  /  s ]_ N )
 
Theoremcdleme41fva11 29933* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  R  =/=  S )  ->  ( F `  R )  =/=  ( F `  S ) )
 
Theoremcdleme42b 29934* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( X  e.  B  /\  ( P  =/=  Q 
 /\  -.  X  .<_  W ) )  /\  (
 ( R  e.  A  /\  -.  R  .<_  W ) 
 /\  ( R  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( F `  X )  =  (
 [_ R  /  s ]_ N  .\/  ( X 
 ./\  W ) ) )
 
Theoremcdleme42e 29935* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  ( R  .\/  V ) )  =  ( [_ R  /  s ]_ N  .\/  ( ( R  .\/  V )  ./\ 
 W ) ) )
 
Theoremcdleme42f 29936* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  ( R  .\/  V ) )  =  (
 ( F `  R )  .\/  V ) )
 
Theoremcdleme42g 29937* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  ( R  .\/  S ) )  =  (
 ( F `  R )  .\/  V ) )
 
Theoremcdleme42h 29938* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  S )  .<_  ( ( F `  R ) 
 .\/  V ) )
 
Theoremcdleme42i 29939* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  P  =/=  Q )  ->  ( ( F `  R )  .\/  ( F `  S ) )  .<_  ( ( F `
  R )  .\/  V ) )
 
Theoremcdleme42k 29940* Part of proof of Lemma E in [Crawley] p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i 29939 and ps-1 28933 TODO: FIX COMMENT (Contributed by NM, 20-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  R  =/=  S )  ->  ( ( F `  R )  .\/  ( F `  S ) )  =  ( ( F `  R ) 
 .\/  V ) )
 
Theoremcdleme42ke 29941* Part of proof of Lemma E in [Crawley] p. 113. Remove  R  =/=  S condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) )  ->  (
 ( F `  R )  .\/  ( F `  S ) )  =  ( ( F `  R )  .\/  V ) )
 
Theoremcdleme42keg 29942* Part of proof of Lemma E in [Crawley] p. 113. Remove  P  =/=  Q condition. TODO: FIX COMMENT TODO: Use instead of cdleme42ke 29941 and even combine with it? (Contributed by NM, 22-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) )  ->  (
 ( F `  R )  .\/  ( F `  S ) )  =  ( ( F `  R )  .\/  V ) )
 
Theoremcdleme42mN 29943* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r  \/ s) = f(r)  \/ s, p. 115 10th line from bottom. (Contributed by NM, 20-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  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) )  ->  ( F `  ( R  .\/  S ) )  =  (
 ( F `  R )  .\/  ( F `  S ) ) )
 
Theoremcdleme42mgN 29944* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r  \/ s) = f(r)  \/ s, p. 115 10th line from bottom. TODO: Use instead of cdleme42mN 29943? Combine with cdleme42mN 29943? (Contributed by NM, 20-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  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  E  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) )  ->  ( F `  ( R  .\/  S ) )  =  ( ( F `  R )  .\/  ( F `  S ) ) )
 
Theoremcdleme43aN 29945 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1) (Contributed by NM, 20-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 )   &    |-  X  =  ( ( Q  .\/  P )  ./\  W )   &    |-  C  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( C  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  D  =  ( ( S  .\/  X )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( Q  .\/  P )  ./\  ( D  .\/  ( ( Z  .\/  S )  ./\  W )
 ) )   &    |-  E  =  ( ( D  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  D )  ./\  W )
 ) )   &    |-  V  =  ( ( Z  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  D )  ./\  W )   =>    |-  (
 ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  G  =  ( ( P  .\/  Q )  ./\  ( D  .\/  V ) ) )
 
Theoremcdleme43bN 29946 Lemma for Lemma E in [Crawley] p. 113. g(s) is an atom not under w. (Contributed by NM, 20-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 )   &    |-  X  =  ( ( Q  .\/  P )  ./\  W )   &    |-  C  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( C  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  D  =  ( ( S  .\/  X )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( Q  .\/  P )  ./\  ( D  .\/  ( ( Z  .\/  S )  ./\  W )
 ) )   &    |-  E  =  ( ( D  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  D )  ./\  W )
 ) )   &    |-  V  =  ( ( Z  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  D )  ./\  W )   =>    |-  (
 ( ( ( 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 )
 )  ->  ( D  e.  A  /\  -.  D  .<_  W ) )
 
Theoremcdleme43cN 29947 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v2 (Contributed by NM, 20-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 )   &    |-  X  =  ( ( Q  .\/  P )  ./\  W )   &    |-  C  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( C  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  D  =  ( ( S  .\/  X )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( Q  .\/  P )  ./\  ( D  .\/  ( ( Z  .\/  S )  ./\  W )
 ) )   &    |-  E  =  ( ( D  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  D )  ./\  W )
 ) )   &    |-  V  =  ( ( Z  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  D )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  -.  S  .<_  ( P  .\/  Q ) )  ->  ( R 
 .\/  D )  =  ( R  .\/  Y )
 )
 
Theoremcdleme43dN 29948 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 116 2nd line: f(r) v s = f(r) v f(g(s)) (Contributed by NM, 20-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 )   &    |-  X  =  ( ( Q  .\/  P )  ./\  W )   &    |-  C  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( C  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  D  =  ( ( S  .\/  X )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( Q  .\/  P )  ./\  ( D  .\/  ( ( Z  .\/  S )  ./\  W )
 ) )   &    |-  E  =  ( ( D  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  D )  ./\  W )
 ) )   &    |-  V  =  ( ( Z  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  D )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  ( Z  .\/  S )  =  ( Z  .\/  E ) )
 
Theoremcdleme46f2g2 29949 Conversion for  G to reuse  F theorems. TODO FIX COMMENT TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 29973? Find other hlatjcom 28824 uses giving  Q 
.\/  P. (Contributed by NM, 1-Apr-2013.)
 |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( ( ( 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 )
 )  ->  ( (
 ( K  e.  HL  /\  W  e.  H ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 /\  ( Q  =/=  P 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  -.  S  .<_  ( Q  .\/  P ) ) )
 
Theoremcdleme46f2g1 29950 Conversion for  G to reuse  F theorems. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)
 |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( ( ( 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 )
 ) )  ->  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 /\  ( Q  =/=  P 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( R  .<_  ( Q  .\/  P )  /\  -.  S  .<_  ( Q 
 .\/  P ) ) ) )
 
Theoremcdleme17d2 29951* Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph.  F,  G represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  -.  S  .<_  ( P  .\/  Q )
 )  ->  ( F `  P )  =  Q )
 
Theoremcdleme17d3 29952* TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q )  ->  ( F `  P )  =  Q )
 
Theoremcdleme17d4 29953* TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =  Q )  ->  ( F `  P )  =  Q )
 
Theoremcdleme17d 29954* Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. We show, in their notation, fs(p)=q. TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  ( F `  P )  =  Q )
 
Theoremcdleme48fv 29955* Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 29897? TODO: Can this be used to help prove the  R or  S case where  X is an atom? (Contributed by NM, 8-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  .\/  ( X 
 ./\  W ) )  =  X ) )  ->  ( F `  X )  =  ( ( F `
  S )  .\/  ( X  ./\  W ) ) )
 
Theoremcdleme48fvg 29956* Remove  P  =/=  Q condition in cdleme48fv 29955. TODO: Can this replace uses of cdleme32a 29897? TODO: Can this be used to help prove the  R or  S case where  X is an atom? TODO: Can this be proved more directly by eliminating  P  =/=  Q in earlier theorems? Should this replace uses of cdleme48fv 29955? (Contributed by NM, 23-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S 
 .\/  ( X  ./\  W ) )  =  X ) )  ->  ( F `
  X )  =  ( ( F `  S )  .\/  ( X 
 ./\  W ) ) )
 
Theoremcdleme46fvaw 29957* Show that  ( F `  R ) is an atom not under  W when  R is an atom not under  W. (Contributed by NM, 18-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 ->  ( ( F `  R )  e.  A  /\  -.  ( F `  R )  .<_  W ) )
 
Theoremcdleme48bw 29958* TODO: fix comment. TODO: Remove unnecessary  P  =/=  Q from cdleme48bw 29958 cdlemeg46c 29969 cdlemeg46fvaw 29972 cdlemeg46rgv 29984 cdlemeg46gfv 29986? cdleme48d 29991? and possibly others they affect. (Contributed by NM, 9-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  .\/  ( X 
 ./\  W ) )  =  X ) )  ->  -.  ( F `  X )  .<_  W )
 
Theoremcdleme48b 29959* TODO: fix comment. (Contributed by NM, 8-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B A.