HomeHome Metamath Proof Explorer
Theorem List (p. 312 of 328)
< 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-22421)
  Hilbert Space Explorer  Hilbert Space Explorer
(22422-23944)
  Users' Mathboxes  Users' Mathboxes
(23945-32762)
 

Theorem List for Metamath Proof Explorer - 31101-31200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme19b 31101 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line.  D,  F,  G represent s2, f(s), f(t). In their notation, we prove that if r 
<_ s  \/ t, then s2  <_ f(s)  \/ f(t). (Contributed by NM, 13-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 )   =>    |-  (
 ( ( ( 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 ) 
 /\  R  e.  A )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  R  .<_  ( S 
 .\/  T ) ) ) )  ->  D  .<_  ( F  .\/  G )
 )
 
Theoremcdleme19c 31102 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line.  D,  F represent s2, f(s). We prove f(s)  =/= s2. (Contributed by NM, 13-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 )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R  e.  A  /\  P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q ) ) )  ->  F  =/=  D )
 
Theoremcdleme19d 31103 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114.  D,  F,  G represent s2, f(s), f(t). We prove f(s)  \/ s2 = f(s)  \/ f(t). (Contributed by NM, 14-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 )   =>    |-  (
 ( ( ( 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 ) 
 /\  R  e.  A )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  R  .<_  ( S 
 .\/  T ) ) ) )  ->  ( F  .\/  D )  =  ( F  .\/  G )
 )
 
Theoremcdleme19e 31104 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 2.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We prove f(s)  \/ s2=f(t)  \/ t2. (Contributed by NM, 14-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 )   =>    |-  (
 ( ( ( 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 ) 
 /\  R  e.  A )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  R  .<_  ( S 
 .\/  T ) ) ) )  ->  ( F  .\/  D )  =  ( G  .\/  Y )
 )
 
Theoremcdleme19f 31105 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 3.  D,  F,  N,  Y,  G,  O represent s2, f(s), fs(r), t2, f(t), ft(r). We prove that if r  <_ s  \/ t, then ft(r) = ft(r). (Contributed by NM, 14-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 ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  R  e.  A )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  R  .<_  ( S 
 .\/  T ) ) ) )  ->  N  =  O )
 
Theoremcdleme20aN 31106 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 14-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( V  .\/  D )  =  ( ( ( S  .\/  R )  .\/  T )  ./\  W ) )
 
Theoremcdleme20bN 31107 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We show v  \/ s2 = v  \/ t2. (Contributed by NM, 15-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( V  .\/  D )  =  ( V  .\/  Y ) )
 
Theoremcdleme20c 31108 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 15-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  T  e.  A )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( D  .\/  Y )  =  ( (
 ( R  .\/  S )  .\/  T )  ./\  W ) )
 
Theoremcdleme20d 31109 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 17-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 )   &    |-  V  =  ( ( 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  /\  -.  T  .<_  W ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )
 )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( F  .\/  G )  ./\  ( D  .\/  Y ) )  =  V )
 
Theoremcdleme20e 31110 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We show <f(s),s2,s> and <f(t),t2,t> are centrally perspective. (Contributed by NM, 17-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 )   &    |-  V  =  ( ( 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  /\  -.  T  .<_  W ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )
 )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( F  .\/  G )  ./\  ( D  .\/  Y ) )  .<_  ( S 
 .\/  T ) )
 
Theoremcdleme20f 31111 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We show <f(s),s2,s> and <f(t),t2,t> are axially perspective. (Contributed by NM, 17-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 )   &    |-  V  =  ( ( 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  /\  -.  T  .<_  W ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )
 )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( F  .\/  D )  ./\  ( G  .\/  Y ) )  .<_  ( ( ( D  .\/  S )  ./\  ( Y  .\/  T ) )  .\/  (
 ( S  .\/  F )  ./\  ( T  .\/  G ) ) ) )
 
Theoremcdleme20g 31112 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 18-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 )   &    |-  V  =  ( ( 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  /\  -.  T  .<_  W ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )
 )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( ( D  .\/  S )  ./\  ( Y  .\/  T ) )  .\/  ( ( S  .\/  F )  ./\  ( T  .\/  G ) ) )  =  ( ( ( S  .\/  R )  ./\  ( T  .\/  R ) )  .\/  ( ( S  .\/  U )  ./\  ( T  .\/  U ) ) ) )
 
Theoremcdleme20h 31113 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 18-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  ( -.  R  .<_  ( S  .\/  T )  /\  -.  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( ( ( S 
 .\/  R )  ./\  ( T  .\/  R ) ) 
 .\/  ( ( S 
 .\/  U )  ./\  ( T  .\/  U ) ) )  =  ( R 
 .\/  U ) )
 
Theoremcdleme20i 31114 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We show (f(s)  \/ s2)  /\ (f(t)  \/ t2)  <_ p  \/ q. (Contributed by NM, 18-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  ( -.  R  .<_  ( S  .\/  T )  /\  -.  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( ( F  .\/  D )  ./\  ( G  .\/  Y ) )  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme20j 31115 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114.  D,  F,  Y,  G represent s2, f(s), t2, f(t). We show s2  =/= t2. (Contributed by NM, 18-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  -.  R  .<_  ( S  .\/  T ) ) )  ->  D  =/=  Y )
 
Theoremcdleme20k 31116 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 20-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  e.  A  /\  Q  e.  A )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  ( F  .\/  D )  =/=  ( P  .\/  Q ) )
 
Theoremcdleme20l1 31117 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  S  e.  A  /\  -.  S  .<_  W )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q )
 ) )  ->  ( F  .\/  D )  e.  ( LLines `  K )
 )
 
Theoremcdleme20l2 31118 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  ( -.  R  .<_  ( S  .\/  T )  /\  -.  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( ( F  .\/  D )  ./\  ( G  .\/  Y ) )  e.  A )
 
Theoremcdleme20l 31119 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line.  D,  F,  Y,  G represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-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 )   &    |-  V  =  ( ( S  .\/  T )  ./\  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 ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  ( -.  R  .<_  ( S  .\/  T )  /\  -.  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( ( F  .\/  D )  ./\  ( G  .\/  Y ) )  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) ) )
 
Theoremcdleme20m 31120 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. 
D,  F,  N,  Y,  G,  O represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. We prove that if  -. r  <_ s  \/ t and  -. u  <_ s  \/ t, then fs(r) = ft(r). (Contributed by NM, 20-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 )   &    |-  V  =  ( ( S  .\/  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 ) )  /\  ( -.  R  .<_  ( S  .\/  T )  /\  -.  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  N  =  O )
 
Theoremcdleme20 31121 Combine cdleme19f 31105 and cdleme20m 31120 to eliminate  -.  R  .<_  ( S  .\/  T ) condition. (Contributed by NM, 28-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 )   &    |-  V  =  ( ( S  .\/  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 ) )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  N  =  O )
 
Theoremcdleme21a 31122 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( S  e.  A  /\  -.  S  .<_  ( P 
 .\/  Q ) )  /\  ( z  e.  A  /\  ( P  .\/  z
 )  =  ( S 
 .\/  z ) ) )  ->  S  =/=  z )
 
Theoremcdleme21b 31123 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( S  e.  A  /\  P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q ) )  /\  (
 z  e.  A  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) 
 ->  -.  z  .<_  ( P 
 .\/  Q ) )
 
Theoremcdleme21c 31124 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-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 )  /\  ( S  e.  A  /\  P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q ) )  /\  (
 z  e.  A  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) 
 ->  -.  U  .<_  ( S 
 .\/  z ) )
 
Theoremcdleme21at 31125 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-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 )  /\  ( ( S  e.  A  /\  P  =/=  Q  /\  -.  S  .<_  ( P 
 .\/  Q ) )  /\  U  .<_  ( S  .\/  T ) )  /\  (
 z  e.  A  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) 
 ->  T  =/=  z )
 
Theoremcdleme21ct 31126 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-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 )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q )  /\  U  .<_  ( S  .\/  T )
 ) )  /\  (
 ( z  e.  A  /\  -.  z  .<_  W ) 
 /\  ( P  .\/  z )  =  ( S  .\/  z ) ) )  ->  -.  U  .<_  ( T  .\/  z )
 )
 
Theoremcdleme21d 31127 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line.  D,  F,  N,  E,  B,  Z represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove fs(r) = fz(r). (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 )
 ) )   &    |-  B  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  E  =  ( ( R  .\/  z )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( B  .\/  E ) )   =>    |-  ( ( ( ( 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  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q )
 )  /\  ( (
 z  e.  A  /\  -.  z  .<_  W )  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) )  ->  N  =  Z )
 
Theoremcdleme21e 31128 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line.  Y,  G,  O,  E,  B,  Z represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove that if u  <_ s  \/ z, then ft(r) = fz(r). (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 )
 ) )   &    |-  B  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  E  =  ( ( R  .\/  z )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( B  .\/  E ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( 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 ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) )  /\  ( ( z  e.  A  /\  -.  z  .<_  W )  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) )  ->  O  =  Z )
 
Theoremcdleme21f 31129 Part of proof of Lemma E in [Crawley] p. 115. (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 )
 ) )   &    |-  B  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  E  =  ( ( R  .\/  z )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( B  .\/  E ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( 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 ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) )  /\  ( ( z  e.  A  /\  -.  z  .<_  W )  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) )  ->  N  =  O )
 
Theoremcdleme21g 31130 Part of proof of Lemma E in [Crawley] p. 115. (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 ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) )  /\  ( ( z  e.  A  /\  -.  z  .<_  W )  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) )  ->  N  =  O )
 
Theoremcdleme21h 31131* Part of proof of Lemma E in [Crawley] p. 115. (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 ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( E. z  e.  A  ( -.  z  .<_  W  /\  ( P 
 .\/  z )  =  ( S  .\/  z
 ) )  ->  N  =  O ) )
 
Theoremcdleme21i 31132* Part of proof of Lemma E in [Crawley] p. 115. (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 ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) )  ->  N  =  O ) )
 
Theoremcdleme21j 31133* Combine cdleme20 31121 and cdleme21i 31132 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 31134 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 31092 and cdleme21j 31133 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 31135 Eliminate  S  =/=  T condition in cdleme21 31134. (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 31136 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 31137 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 31138 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 31139 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 31140 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 31141 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 31142 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 31143 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 31144 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 31143 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 31145 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 31146 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 31147 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 31148 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 31149* Quantified version of cdleme21k 31135. (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 31150* Lemma for cdleme25b 31151. (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 31151* Transform cdleme24 31149. 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 31152* Transform cdleme25b 31151. (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 31153* Transform cdleme25c 31152. (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 31154* Show closure of the unique element in cdleme25c 31152. (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 31155* Change bound variables in cdleme25c 31152. (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 31156* 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 31157* 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 31158* 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 31159* 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 31160* 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 31161* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31159 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 31162* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31159 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 31163* 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 31164* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 31160 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 31165* Lemma for cdleme27N 31166. (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 31166* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme27a 31164. (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