HomeHome Metamath Proof Explorer
Theorem List (p. 339 of 410)
< 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-26627)
  Hilbert Space Explorer  Hilbert Space Explorer
(26628-28150)
  Users' Mathboxes  Users' Mathboxes
(28151-40909)
 

Theorem List for Metamath Proof Explorer - 33801-33900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremtrlval5 33801 The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( R `  F ) ) 
 ./\  W ) )
 
Theoremarglem1N 33802 Lemma for Desargues' law. Theorem 13.3 of [Crawley] p. 110, 3rd and 4th lines from bottom. In these lemmas,  P,  Q,  R,  S,  T,  U,  C,  D,  E,  F, and  G represent Crawley's a0, a1, a2, b0, b1, b2, c, z0, z1, z2, and p respectively. (Contributed by NM, 28-Jun-2012.) (New usage is discouraged.)
 |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  F  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  G  =  ( ( P  .\/  S )  ./\  ( Q  .\/  T ) )   =>    |-  ( ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  P  =/=  Q )  /\  ( P  =/=  S  /\  Q  =/=  T  /\  S  =/=  T ) )  /\  G  e.  A )  ->  F  e.  A )
 
Theoremcdlemc1 33803 Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 33475? (Contributed by NM, 29-May-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  B  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( ( P  .\/  X )  ./\  W )
 )  =  ( P 
 .\/  X ) )
 
Theoremcdlemc2 33804 Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) )  ->  ( F `  Q )  .<_  ( ( F `  P ) 
 .\/  ( ( P 
 .\/  Q )  ./\  W ) ) )
 
Theoremcdlemc3 33805 Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) )  ->  ( ( F `  P )  .<_  ( Q 
 .\/  ( R `  F ) )  ->  Q  .<_  ( P  .\/  ( F `  P ) ) ) )
 
Theoremcdlemc4 33806 Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  -.  Q  .<_  ( P  .\/  ( F `  P ) ) )  ->  ( Q  .\/  ( R `  F ) )  =/=  ( ( F `  P )  .\/  ( ( P  .\/  Q )  ./\ 
 W ) ) )
 
Theoremcdlemc5 33807 Lemma for cdlemc 33809. (Contributed by NM, 26-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( -.  Q  .<_  ( P  .\/  ( F `  P ) )  /\  ( F `
  P )  =/= 
 P ) )  ->  ( F `  Q )  =  ( ( Q 
 .\/  ( R `  F ) )  ./\  ( ( F `  P )  .\/  ( ( P  .\/  Q )  ./\ 
 W ) ) ) )
 
Theoremcdlemc6 33808 Lemma for cdlemc 33809. (Contributed by NM, 26-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F `  P )  =  P )  ->  ( F `  Q )  =  ( ( Q  .\/  ( R `  F ) )  ./\  ( ( F `  P )  .\/  ( ( P  .\/  Q )  ./\  W )
 ) ) )
 
Theoremcdlemc 33809 Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  -.  Q  .<_  ( P  .\/  ( F `  P ) ) )  ->  ( F `  Q )  =  ( ( Q  .\/  ( R `  F ) )  ./\  ( ( F `  P )  .\/  ( ( P  .\/  Q )  ./\  W )
 ) ) )
 
Theoremcdlemd1 33810 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( R  e.  A  /\  P  =/=  Q  /\  -.  R  .<_  ( P 
 .\/  Q ) ) ) )  ->  R  =  ( ( P  .\/  ( ( P  .\/  R )  ./\  W )
 )  ./\  ( Q  .\/  ( ( Q  .\/  R )  ./\  W )
 ) ) )
 
Theoremcdlemd2 33811 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-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 )  /\  R  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  R  .<_  ( P  .\/  Q )
 ) )  /\  (
 ( F `  P )  =  ( G `  P )  /\  ( F `  Q )  =  ( G `  Q ) ) )  ->  ( F `  R )  =  ( G `  R ) )
 
Theoremcdlemd3 33812 Part of proof of Lemma D in [Crawley] p. 113. The  R  =/=  P requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  R  .<_  ( P 
 .\/  Q )  /\  R  =/=  P ) )  /\  ( R  e.  A  /\  S  e.  A  /\  -.  S  .<_  ( P  .\/  Q ) ) )  ->  -.  R  .<_  ( P  .\/  S ) )
 
Theoremcdlemd4 33813 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-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 )  /\  R  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  R  .<_  ( P 
 .\/  Q )  /\  R  =/=  P ) )  /\  ( ( F `  P )  =  ( G `  P )  /\  ( F `  Q )  =  ( G `  Q ) ) ) 
 ->  ( F `  R )  =  ( G `  R ) )
 
Theoremcdlemd5 33814 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-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 )  /\  R  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  P  =/=  Q )  /\  ( ( F `
  P )  =  ( G `  P )  /\  ( F `  Q )  =  ( G `  Q ) ) )  ->  ( F `  R )  =  ( G `  R ) )
 
Theoremcdlemd6 33815 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 33816 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 33817 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 33818 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 33819 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 33820 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 33821 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 33822 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 33823 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 33824 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 33825 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 33826 Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 34210- swap consequent equality; make antecedent use df-3an 993. (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 33827 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 33828 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 33829 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 33830 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 33831 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 33832 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 33833 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 33834 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 33835* 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 33836* 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 33837* 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 33838 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 33839 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 33840 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 33841 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33842 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33843 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33844 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33845 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. TODO: Delete - duplicates cdleme0e 33829. (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 33846 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33847 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 33848 and cdleme3 33849. (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 33848 Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 33849. (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 33849 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 33848 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 33841 through cdleme3 33849, 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 33850 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 33851 Part of proof of Lemma E in [Crawley] p. 114 top.  G represents fs(r). Auxiliary lemma derived from cdleme5 33852. 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 33852 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 33853 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 33854 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33855 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33856 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33857 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33858 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33859 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33860 and cdleme7 33861. (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 33860 Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 33861. (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 33861 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 33860 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 33854 through cdleme7 33861, 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 33862 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 33863 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 33864 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 33865 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 33866 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 33867 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 33868 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 33869 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 33870 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 33871 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 33872 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33873 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33874 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33875 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33876 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33877 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33878 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33879 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33880 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33881 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33882. (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 33882 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 33872 through cdleme11 33882, 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 33883 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 33884 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 33885 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 33497 to cdleme13 33884. 
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 33886 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 33887 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 33888 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 33889 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 33890 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 33891 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 33892 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 33893 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 33894 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 33895 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 33896 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 33897 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 33898 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 33899 Lemma leading to cdleme17c 33900. (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 33900 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 )
    < 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 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-1690