HomeHome Metamath Proof Explorer
Theorem List (p. 344 of 360)
< 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-24492)
  Hilbert Space Explorer  Hilbert Space Explorer
(24493-26017)
  Users' Mathboxes  Users' Mathboxes
(26018-35975)
 

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemednpq 34301 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma.  D represents s2. (Contributed by NM, 18-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q ) ) )  ->  -.  D  .<_  ( P  .\/  Q ) )
 
TheoremcdlemednuN 34302 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma.  D represents s2. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q ) ) )  ->  D  =/=  U )
 
Theoremcdleme20zN 34303 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( S  =/=  T  /\  -.  R  .<_  ( S 
 .\/  T ) ) ) 
 ->  ( ( S  .\/  R )  ./\  T )  =  ( 0. `  K ) )
 
Theoremcdleme20y 34304 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( S  =/=  T  /\  -.  R  .<_  ( S 
 .\/  T ) ) ) 
 ->  ( ( S  .\/  R )  ./\  ( T  .\/  R ) )  =  R )
 
Theoremcdleme19a 34305 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line.  D represents s2. In their notation, we prove that if r  <_ s  \/ t, then s2=(s  \/ t)  /\ w. (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  /\  ( R  e.  A  /\  S  e.  A  /\  T  e.  A )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( S  .\/  T )
 ) )  ->  D  =  ( ( S  .\/  T )  ./\  W )
 )
 
Theoremcdleme19b 34306 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 34307 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 34308 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 34309 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 34310 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 34311 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 34312 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 34313 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 34314 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 34315 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 34316 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 34317 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 34318 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 34319 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 34320 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 34321 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 34322 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 34323 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 34324 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 34325 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 34326 Combine cdleme19f 34310 and cdleme20m 34325 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 34327 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 34328 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 34329 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 34330 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 34331 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 34332 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 34333 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 34334 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 34335 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 34336* 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 34337* 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 34338* Combine cdleme20 34326 and cdleme21i 34337 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 34339 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 34297 and cdleme21j 34338 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 34340 Eliminate  S  =/=  T condition in cdleme21 34339. (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 34341 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 34342 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 34343 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 34344 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 34345 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 34346 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 34347 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 34348 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 34349 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 34348 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 34350 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 34351 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 34352 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 34353 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 34354* Quantified version of cdleme21k 34340. (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 34355* Lemma for cdleme25b 34356. (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 34356* Transform cdleme24 34354. 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 34357* Transform cdleme25b 34356. (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 34358* Transform cdleme25c 34357. (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 34359* Show closure of the unique element in cdleme25c 34357. (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 34360* Change bound variables in cdleme25c 34357. (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 34361* 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 34362* 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 34363* 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 34364* 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 34365* 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 34366* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 34364 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 34367* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 34364 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 34368* 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 34369* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 34365 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 ) ) )   &    |-