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

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21498)
  Hilbert Space Explorer  Hilbert Space Explorer
(21499-23021)
  Users' Mathboxes  Users' Mathboxes
(23022-32154)
 

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme0b 30401 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-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 )  ->  U  =/=  P )
 
Theoremcdleme0c 30402 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-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  /\  Q  e.  A )  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  ->  U  =/=  R )
 
Theoremcdleme0cp 30403 Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 30786- swap consequent equality; make antecedent use df-3an 936. (Contributed by NM, 13-Jun-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  .\/  U )  =  ( P  .\/  Q )
 )
 
Theoremcdleme0cq 30404 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( 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  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) )  ->  ( Q  .\/  U )  =  ( P  .\/  Q ) )
 
Theoremcdleme0dN 30405 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R  e.  A  /\  P  =/=  R ) )  ->  V  e.  A )
 
Theoremcdleme0e 30406 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P  .\/  Q ) ) )  ->  U  =/=  V )
 
Theoremcdleme0fN 30407 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  R  e.  A ) )  ->  V  =/=  P )
 
Theoremcdleme0gN 30408 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  R  e.  A )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  V  =/=  Q )
 
Theoremcdlemeulpq 30409 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-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  /\  Q  e.  A ) )  ->  U  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme01N 30410 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q )  ->  ( ( U  =/=  P  /\  U  =/=  Q  /\  U  .<_  ( P  .\/  Q )
 )  /\  U  .<_  W ) )
 
Theoremcdleme02N 30411 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q )  ->  ( ( P  .\/  U )  =  ( Q  .\/  U )  /\  U  .<_  W ) )
 
Theoremcdleme0ex1N 30412* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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 ) 
 ->  E. u  e.  A  ( u  .<_  ( P 
 .\/  Q )  /\  u  .<_  W ) )
 
Theoremcdleme0ex2N 30413* Part of proof of Lemma E in [Crawley] p. 113. Note that  ( P  .\/  u )  =  ( Q  .\/  u ) is a shorter way to express  u  =/=  P  /\  u  =/=  Q  /\  u  .<_  ( P 
.\/  Q ). (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q )  ->  E. u  e.  A  ( ( P 
 .\/  u )  =  ( Q  .\/  u )  /\  u  .<_  W ) )
 
Theoremcdleme0moN 30414* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  -.  Q  .<_  W ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  E* r ( r  e.  A  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( R  =  P  \/  R  =  Q ) )
 
Theoremcdleme1b 30415 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma showing  F is a lattice element.  F represents their f(r). (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  B  =  (
 Base `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )
 )  ->  F  e.  B )
 
Theoremcdleme1 30416 Part of proof of Lemma E in [Crawley] p. 113.  F represents their f(r). Here we show r  \/ f(r) = r  \/ u (7th through 5th lines from bottom on p. 113). (Contributed by NM, 4-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  ( R  .\/  F )  =  ( R  .\/  U ) )
 
Theoremcdleme2 30417 Part of proof of Lemma E in [Crawley] p. 113. .  F represents f(r).  W is the fiducial co-atom (hyperplane) w. Here we show that (r  \/ f(r))  /\ w = u in their notation (4th line from bottom on p. 113). (Contributed by NM, 5-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  (
 ( R  .\/  F )  ./\  W )  =  U )
 
Theoremcdleme3b 30418 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  P  =/=  Q )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  F  =/=  R )
 
Theoremcdleme3c 30419 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  .0.  =  ( 0. `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  P  =/=  Q )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  F  =/=  .0.  )
 
Theoremcdleme3d 30420 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  V ) )
 
Theoremcdleme3e 30421 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  ( P  .\/  Q )
 ) ) )  ->  V  e.  A )
 
Theoremcdleme3fN 30422 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. TODO: Delete - duplicates cdleme0e 30406. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  V  =  ( ( P  .\/  R )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P  .\/  Q ) ) )  ->  U  =/=  V )
 
Theoremcdleme3g 30423 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 7-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  V  =  ( ( P  .\/  R )  ./\  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 ) ) )  ->  F  =/=  U )
 
Theoremcdleme3h 30424 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30425 and cdleme3 30426. (Contributed by NM, 6-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   &    |-  V  =  ( ( P  .\/  R )  ./\  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 ) ) )  ->  F  e.  A )
 
Theoremcdleme3fa 30425 Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 30426. (Contributed by NM, 6-Oct-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  R  .<_  ( P  .\/  Q )
 ) )  ->  F  e.  A )
 
Theoremcdleme3 30426 Part of proof of Lemma E in [Crawley] p. 113.  F represents f(r).  W is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 30425 above, we show that f(r)  e. W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as  F  e.  A  /\  -.  F  .<_  W. Their proof provides no details of our lemmas cdleme3b 30418 through cdleme3 30426, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  R  .<_  ( P  .\/  Q )
 ) )  ->  -.  F  .<_  W )
 
Theoremcdleme4 30427 Part of proof of Lemma E in [Crawley] p. 113.  F and  G represent f(s) and fs(r). Here show p  \/ q = r  \/ u at the top of p. 114. (Contributed by NM, 7-Jun-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  /\  Q  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  R  .<_  ( P  .\/  Q )
 )  ->  ( P  .\/  Q )  =  ( R  .\/  U )
 )
 
Theoremcdleme4a 30428 Part of proof of Lemma E in [Crawley] p. 114 top.  G represents fs(r). Auxiliary lemma derived from cdleme5 30429. We show fs(r)  <_ p  \/ q. (Contributed by NM, 10-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  S  e.  A ) 
 ->  G  .<_  ( P  .\/  Q ) )
 
Theoremcdleme5 30429 Part of proof of Lemma E in [Crawley] p. 113.  G represents fs(r). We show r  \/ fs(r)) = p  \/ q at the top of p. 114. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( 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 ) ) )  ->  ( R  .\/  G )  =  ( P  .\/  Q ) )
 
Theoremcdleme6 30430 Part of proof of Lemma E in [Crawley] p. 113. This expresses (r  \/ fs(r))  /\ w = u at the top of p. 114. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( 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 ) ) )  ->  ( ( R  .\/  G )  ./\  W )  =  U )
 
Theoremcdleme7aa 30431 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  -.  R  .<_  ( U  .\/  S ) )
 
Theoremcdleme7a 30432 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  G  =  ( ( P  .\/  Q )  ./\  ( F  .\/  V ) )
 
Theoremcdleme7b 30433 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  V  e.  A )
 
Theoremcdleme7c 30434 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 7-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  U  =/=  V )
 
Theoremcdleme7d 30435 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 8-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  G  =/=  U )
 
Theoremcdleme7e 30436 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30437 and cdleme7 30438. (Contributed by NM, 8-Jun-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  V  =  ( ( R  .\/  S )  ./\  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  G  =/=  ( 0. `  K ) )
 
Theoremcdleme7ga 30437 Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 30438. (Contributed by NM, 8-Jun-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  =  ( ( 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 ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  G  e.  A )
 
Theoremcdleme7 30438 Part of proof of Lemma E in [Crawley] p. 113.  G and  F represent fs(r) and f(s) respectively.  W is the fiducial co-atom (hyperplane) that they call w. Here and in cdleme7ga 30437 above, we show that fs(r)  e. W (top of p. 114), meaning it is an atom and not under w, which in our notation is expressed as  G  e.  A  /\  -.  G  .<_  W. (Note that we do not have a symbol for their W.) Their proof provides no details of our cdleme7aa 30431 through cdleme7 30438, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-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  =  ( ( 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 ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  -.  G  .<_  W )
 
Theoremcdleme8 30439 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  C represents s1. In their notation, we prove p  \/ s1 = p  \/ s. (Contributed by NM, 9-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  S  e.  A )  ->  ( P 
 .\/  C )  =  ( P  .\/  S )
 )
 
Theoremcdleme9a 30440 Part of proof of Lemma E in [Crawley] p. 113.  C represents s1, which we prove is an atom. (Contributed by NM, 10-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( S  e.  A  /\  P  =/=  S ) )  ->  C  e.  A )
 
Theoremcdleme9b 30441 Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  S  e.  A  /\  W  e.  H )
 )  ->  C  e.  B )
 
Theoremcdleme9 30442 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  C and  F represent s1 and f(s) respectively. In their notation, we prove f(s)  \/ s1 = q  \/ s1. (Contributed by NM, 10-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  -.  S  .<_  ( P  .\/  Q ) )  ->  ( F  .\/  C )  =  ( Q  .\/  C ) )
 
Theoremcdleme10 30443 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  D represents s2. In their notation, we prove s  \/ s2 = s  \/ r. (Contributed by NM, 9-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  R  e.  A  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  ->  ( S  .\/  D )  =  ( S  .\/  R )
 )
 
Theoremcdleme8tN 30444 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  X represents t1. In their notation, we prove p  \/ t1 = p  \/ t. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  X  =  ( ( P  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  T  e.  A )  ->  ( P 
 .\/  X )  =  ( P  .\/  T )
 )
 
Theoremcdleme9taN 30445 Part of proof of Lemma E in [Crawley] p. 113.  X represents t1, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  X  =  ( ( P  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( T  e.  A  /\  P  =/=  T ) )  ->  X  e.  A )
 
Theoremcdleme9tN 30446 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  X and  F represent t1 and f(t) respectively. In their notation, we prove f(t)  \/ t1 = q  \/ t1. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  X  =  ( ( P  .\/  T )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  -.  T  .<_  ( P  .\/  Q ) )  ->  ( F  .\/  X )  =  ( Q  .\/  X ) )
 
Theoremcdleme10tN 30447 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114.  Y represents t2. In their notation, we prove t  \/ t2 = t  \/ r. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  R  e.  A  /\  ( T  e.  A  /\  -.  T  .<_  W ) )  ->  ( T  .\/  Y )  =  ( T  .\/  R )
 )
 
Theoremcdleme16aN 30448 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s  \/ u  =/= t  \/ u. (Contributed by NM, 9-Oct-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  T  e.  A ) 
 /\  ( P  =/=  Q 
 /\  S  =/=  T  /\  -.  U  .<_  ( S 
 .\/  T ) ) ) 
 ->  ( S  .\/  U )  =/=  ( T  .\/  U ) )
 
Theoremcdleme11a 30449 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 12-Jun-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 ) )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( S  .\/  U )  =  ( S  .\/  T ) )
 
Theoremcdleme11c 30450 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 13-Jun-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  /\  P  =/=  Q )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  U  .<_  ( S 
 .\/  T ) ) ) 
 ->  -.  P  .<_  ( S 
 .\/  T ) )
 
Theoremcdleme11dN 30451 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  P  =/=  Q )  /\  ( S  =/=  T 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) )  ->  ( P  .\/  S )  =/=  ( P  .\/  T ) )
 
Theoremcdleme11e 30452 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 13-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A  /\  P  =/=  Q )  /\  ( S  =/=  T 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) )  ->  C  =/=  D )
 
Theoremcdleme11fN 30453 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  F  =/=  C )
 
Theoremcdleme11g 30454 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 14-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  S  e.  A )  /\  P  =/=  Q )  ->  ( Q  .\/  F )  =  ( Q 
 .\/  C ) )
 
Theoremcdleme11h 30455 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 14-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  S  e.  A )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P  .\/  Q ) ) )  ->  F  =/=  Q )
 
Theoremcdleme11j 30456 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 14-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  C  .<_  ( Q  .\/  F ) )
 
Theoremcdleme11k 30457 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 15-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  D  =  ( ( P  .\/  T )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  C  =  ( ( Q  .\/  F )  ./\  W )
 )
 
Theoremcdleme11l 30458 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30459. (Contributed by NM, 15-Jun-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  U  .<_  ( S  .\/  T )
 ) )  ->  F  =/=  G )
 
Theoremcdleme11 30459 Part of proof of Lemma E in [Crawley] p. 113, 1st sentence of 3rd paragraph on p. 114.  F and  G represent f(s) and f(t) respectively. Their proof provides no details of our cdleme11a 30449 through cdleme11 30459, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  U  .<_  ( S  .\/  T )
 ) )  ->  ( F  .\/  G )  =  ( S  .\/  T ) )
 
Theoremcdleme12 30460 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. 
F and  G represent f(s) and f(t) respectively. (Contributed by NM, 16-Jun-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 )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A  /\  P  =/=  Q ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( S  =/=  T 
 /\  -.  U  .<_  ( S  .\/  T )
 ) ) )  ->  ( ( S  .\/  F )  ./\  ( T  .\/  G ) )  =  U )
 
Theoremcdleme13 30461 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> are centrally perspective."  F and  G represent f(s) and f(t) respectively. (Contributed by NM, 7-Oct-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 )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A  /\  P  =/=  Q ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( S  =/=  T 
 /\  -.  U  .<_  ( S  .\/  T )
 ) ) )  ->  ( ( S  .\/  F )  ./\  ( T  .\/  G ) )  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme14 30462 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> ... are axially perspective." We apply dalaw 30075 to cdleme13 30461. 
F and  G represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  ( F  .\/  G ) )  .<_  ( ( ( T  .\/  P )  ./\  ( G  .\/  Q ) )  .\/  ( ( P  .\/  S )  ./\  ( Q  .\/  F ) ) ) )
 
Theoremcdleme15a 30463 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((s  \/ p)  /\ (f(s)  \/ q))  \/ ((t  \/ p)  /\ (f(t)  \/ q))=((p  \/ s1)  /\ (q  \/ s1))  \/ ((p  \/ t1)  /\ (q 
\/ t1)). We represent f(s), f(t), s1, and t1 with  F,  G,  C, and  X respectively. The order of our operations is slightly different. (Contributed by NM, 9-Oct-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 )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  X  =  ( ( P  .\/  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 ) 
 /\  ( P  =/=  Q 
 /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T )
 ) )  ->  (
 ( ( T  .\/  P )  ./\  ( G  .\/  Q ) )  .\/  ( ( P  .\/  S )  ./\  ( Q  .\/  F ) ) )  =  ( ( ( P  .\/  X )  ./\  ( Q  .\/  X ) )  .\/  ( ( P  .\/  C )  ./\  ( Q  .\/  C ) ) ) )
 
Theoremcdleme15b 30464 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (p  \/ s1)  /\ (q  \/ s1)=s1. We represent s1 with  C. (Contributed by NM, 10-Oct-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 )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  X  =  ( ( P  .\/  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 ) 
 /\  ( P  =/=  Q 
 /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T )
 ) )  ->  (
 ( P  .\/  C )  ./\  ( Q  .\/  C ) )  =  C )
 
Theoremcdleme15c 30465 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p  \/ s1)  /\ (q  \/ s1))  \/ ((p  \/ t1)  /\ (q  \/ t1))=s1  \/ t1.  C and  X represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-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 )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  X  =  ( ( P  .\/  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 ) 
 /\  ( P  =/=  Q 
 /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T )
 ) )  ->  (
 ( ( P  .\/  X )  ./\  ( Q  .\/  X ) )  .\/  ( ( P  .\/  C )  ./\  ( Q  .\/  C ) ) )  =  ( X  .\/  C ) )
 
Theoremcdleme15d 30466 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s1  \/ t1  <_ w.  C and  X represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-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 )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   &    |-  X  =  ( ( P  .\/  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 ) 
 /\  ( P  =/=  Q 
 /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T )
 ) )  ->  ( X  .\/  C )  .<_  W )
 
Theoremcdleme15 30467 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (s  \/ t)  /\ (f(s)  \/ f(t))  <_ w. We use  F,  G for f(s), f(t) respectively. (Contributed by NM, 10-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  ( F  .\/  G ) )  .<_  W )
 
Theoremcdleme16b 30468 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. 
F and  G represent f(s) and f(t) respectively. It is unclear how this follows from s  \/ u  =/= t  \/ u, as the authors state, and we used a different proof. (Note: the antecedent  -.  T  .<_  ( P 
.\/  Q ) is not used.) (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  F  =/=  G )
 
Theoremcdleme16c 30469 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 2nd part of 3rd sentence.  F and  G represent f(s) and f(t) respectively. We show, in their notation, s  \/ t 
\/ f(s)  \/ f(t)=s  \/ t  \/ u. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  .\/  ( F  .\/  G ) )  =  ( ( S  .\/  T )  .\/  U )
 )
 
Theoremcdleme16d 30470 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence.  F and  G represent f(s) and f(t) respectively. We show, in their notation, (s  \/ t)  /\ (f(s)  \/ f(t)) is an atom. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  ( F  .\/  G ) )  e.  A )
 
Theoremcdleme16e 30471 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence.  F and  G represent f(s) and f(t) respectively. We show, in their notation, (s  \/ t)  /\ (f(s)  \/ f(t))=(s  \/ t)  /\ w. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  ( F  .\/  G ) )  =  ( ( S  .\/  T )  ./\  W )
 )
 
Theoremcdleme16f 30472 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence.  F and  G represent f(s) and f(t) respectively. We show, in their notation, (s  \/ t)  /\ (f(s)  \/ f(t))=(f(s)  \/ f(t))  /\ w. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  ( F  .\/  G ) )  =  ( ( F  .\/  G )  ./\  W )
 )
 
Theoremcdleme16g 30473 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, Eq. (1).  F and  G represent f(s) and f(t) respectively. We show, in their notation, (s 
\/ t)  /\ w=(f(s)  \/ f(t))  /\ w. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  -.  U  .<_  ( S  .\/  T ) ) )  ->  ( ( S  .\/  T )  ./\  W )  =  ( ( F  .\/  G )  ./\  W )
 )
 
Theoremcdleme16 30474 Part of proof of Lemma E in [Crawley] p. 113, conclusion of 3rd paragraph on p. 114.  F and  G represent f(s) and f(t) respectively. We show, in their notation, (s  \/ t)  /\ w=(f(s)  \/ f(t))  /\ w, whether or not u  <_ s  \/ t. (Contributed by NM, 11-Oct-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 )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W )  /\  ( P  =/=  Q  /\  S  =/=  T ) )  /\  ( -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) ) )  ->  ( ( S  .\/  T )  ./\  W )  =  ( ( F  .\/  G )  ./\  W )
 )
 
Theoremcdleme17a 30475 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph.  F,  G, and  C represent f(s), fs(p), and s1 respectively. We show, in their notation, fs(p)=(p  \/ q)  /\ (q  \/ s1). (Contributed by NM, 11-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  -.  S  .<_  ( P  .\/  Q ) )  ->  G  =  ( ( P  .\/  Q )  ./\  ( Q  .\/  C ) ) )
 
Theoremcdleme17b 30476 Lemma leading to cdleme17c 30477. (Contributed by NM, 11-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  S  e.  A  /\  -.  S  .<_  ( P 
 .\/  Q ) ) ) 
 ->  -.  C  .<_  ( P 
 .\/  Q ) )
 
Theoremcdleme17c 30477 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph.  C represents s1. We show, in their notation, (p  \/ q)  /\ (q  \/ s1)=q. (Contributed by NM, 11-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  C  =  ( ( P  .\/  S )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  S  e.  A  /\  -.  S  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( ( P  .\/  Q )  ./\  ( Q  .\/  C ) )  =  Q )
 
Theoremcdleme17d1 30478 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph.  F,  G represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. (Contributed by NM, 11-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  Q  e.  A  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  -.  S  .<_  ( P  .\/  Q ) )  ->  G  =  Q )
 
Theoremcdleme0nex 30479* Part of proof of Lemma E in [Crawley] p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p  \/ q/0 (i.e. the sublattice from 0 to p  \/ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a 30400- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 29533, our  ( P  .\/  r )  =  ( Q  .\/  r ) is a shorter way to express  r  =/=  P  /\  r  =/=  Q  /\  r  .<_  ( P 
.\/  Q ). Thus the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  R  .<_  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) 
 /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  ->  ( R  =  P  \/  R  =  Q )
 )
 
Theoremcdleme18a 30480 Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph.  F,  G represent f(s), fs(q) respectively. We show  -. fs(q)  <_ w. (Contributed by NM, 12-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  -.  G  .<_  W )
 
Theoremcdleme18b 30481 Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph.  F,  G represent f(s), fs(q) respectively. We show  -. fs(q)  =/= q. (Contributed by NM, 12-Oct-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  G  =/=  Q )
 
Theoremcdleme18c 30482* Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph.  F,  G represent f(s), fs(q) respectively. We show  -. fs(q) = p whenever p  \/ q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  G  =  P )
 
Theoremcdleme22gb 30483 Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  B  =  (
 Base `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A ) 
 /\  ( R  e.  A  /\  S  e.  A ) )  ->  G  e.  B )
 
Theoremcdleme18d 30484* Part of proof of Lemma E in [Crawley] p. 114, 4th sentence of 4th paragraph.  F,  G,  D,  E represent f(s), fs(r), f(t), ft(r) respectively. We show fs(r)=ft(r) for all possible r (which must equal p or q in the case of exactly 3 atoms in p  \/ q/0 i.e. when  -.  E. r  e.  A...). (Contributed by NM, 12-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  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   &    |-  D  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  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 
 /\  ( R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P 
 .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q ) )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  G  =  E )
 
Theoremcdlemesner 30485 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( K  e.  HL  /\  ( R  e.  A  /\  S  e.  A ) 
 /\  ( R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P 
 .\/  Q ) ) ) 
 ->  S  =/=  R )
 
Theoremcdlemedb 30486 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma.  D represents s2. (Contributed by NM, 20-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  S  e.  A ) )  ->  D  e.  B )
 
Theoremcdlemeda 30487 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma.  D represents s2. (Contributed by NM, 13-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( R  e.  A  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  D  e.  A )
 
Theoremcdlemednpq 30488 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 30489 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 30490 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 30491 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 30492 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 30493 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 30494 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 30495 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 30496 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 30497 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 )