HomeHome Metamath Proof Explorer
Theorem List (p. 310 of 327)
< 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-22411)
  Hilbert Space Explorer  Hilbert Space Explorer
(22412-23934)
  Users' Mathboxes  Users' Mathboxes
(23935-32663)
 

Theorem List for Metamath Proof Explorer - 30901-31000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemd6 30901 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  -.  Q  .<_  ( P  .\/  ( F `  P ) ) ) 
 /\  ( F `  P )  =  ( G `  P ) ) 
 ->  ( F `  Q )  =  ( G `  Q ) )
 
Theoremcdlemd7 30902 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  R  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( F `  P )  =  ( G `  P )  /\  -.  Q  .<_  ( P  .\/  ( F `  P ) ) ) )  ->  ( F `  R )  =  ( G `  R ) )
 
Theoremcdlemd8 30903 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  R  e.  A )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( F `  P )  =  ( G `  P )  /\  ( F `
  P )  =  P ) )  ->  ( F `  R )  =  ( G `  R ) )
 
Theoremcdlemd9 30904 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  R  e.  A )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F `
  P )  =  ( G `  P ) )  ->  ( F `
  R )  =  ( G `  R ) )
 
Theoremcdlemd 30905 If two translations agree at any atom not under the fiducial co-atom  W, then they are equal. Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F `
  P )  =  ( G `  P ) )  ->  F  =  G )
 
Theoremltrneq3 30906 Two translations agree at any atom not under the fiducial co-atom  W iff they are equal. (Contributed by NM, 25-Jul-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( F `  P )  =  ( G `  P )  <->  F  =  G ) )
 
Theoremcdleme00a 30907 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  -.  R  .<_  ( P 
 .\/  Q ) )  ->  R  =/=  P )
 
Theoremcdleme0aa 30908 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  P  e.  A  /\  Q  e.  A ) 
 ->  U  e.  B )
 
Theoremcdleme0a 30909 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  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  P  =/=  Q ) )  ->  U  e.  A )
 
Theoremcdleme0b 30910 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 30911 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 30912 Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 31295- swap consequent equality; make antecedent use df-3an 938. (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 30913 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 30914 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 30915 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 30916 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 30917 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 30918 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 30919 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 30920 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 30921* 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 30922* 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 30923* 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 30924 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 30925 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 30926 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 30927 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30928 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30929 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30930 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30931 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. TODO: Delete - duplicates cdleme0e 30915. (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 30932 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30933 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 30934 and cdleme3 30935. (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 30934 Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 30935. (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 30935 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 30934 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 30927 through cdleme3 30935, 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 30936 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 30937 Part of proof of Lemma E in [Crawley] p. 114 top.  G represents fs(r). Auxiliary lemma derived from cdleme5 30938. 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 30938 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 30939 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 30940 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30941 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30942 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30943 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30944 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30945 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 30946 and cdleme7 30947. (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 30946 Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 30947. (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 30947 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 30946 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 30940 through cdleme7 30947, 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 30948 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 30949 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 30950 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 30951 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 30952 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 30953 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 30954 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 30955 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 30956 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 30957 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 30958 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30959 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30960 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30961 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30962 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30963 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30964 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30965 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30966 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30967 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 30968. (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 30968 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 30958 through cdleme11 30968, 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 30969 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 30970 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 30971 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 30584 to cdleme13 30970. 
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 30972 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 30973 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 30974 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 30975 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 30976 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 30977 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 30978 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 30979 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 30980 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 30981 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 30982 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 30983 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 30984 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 30985 Lemma leading to cdleme17c 30986. (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 30986 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 30987 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 30988* 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 30909- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 30042, 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 30989 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 30990 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 30991* 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 30992 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 30993* 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 30994 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 30995 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 30996 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 30997 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 30998 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 30999 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 31000 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 )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122