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

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21514)
  Hilbert Space Explorer  Hilbert Space Explorer
(21515-23037)
  Users' Mathboxes  Users' Mathboxes
(23038-32776)
 

Theorem List for Metamath Proof Explorer - 31001-31100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremarglem1N 31001 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 31002 Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 30675? (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 31003 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 31004 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 31005 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 31006 Lemma for cdlemc 31008. (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 31007 Lemma for cdlemc 31008. (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 31008 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 31009 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 31010 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 31011 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 31012 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 31013 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 31014 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 31015 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 31016 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 31017 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 31018 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 31019 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 31020 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 31021 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 31022 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 31023 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 31024 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 31025 Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 31408- swap consequent equality; make antecedent use df-3an 936. (Contributed by NM, 13-Jun-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A )
 )  ->  ( P  .\/  U )  =  ( P  .\/  Q )
 )
 
Theoremcdleme0cq 31026 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 31027 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 31028 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 31029 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 31030 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 31031 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 31032 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 31033 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 31034* 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 31035* 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 31036* 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 31037 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 31038 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 31039 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 31040 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31041 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31042 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31043 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31044 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. TODO: Delete - duplicates cdleme0e 31028. (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 31045 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31046 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31047 and cdleme3 31048. (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 31047 Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 31048. (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 31048 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 31047 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 31040 through cdleme3 31048, 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 31049 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 31050 Part of proof of Lemma E in [Crawley] p. 114 top.  G represents fs(r). Auxiliary lemma derived from cdleme5 31051. 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 31051 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 31052 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 31053 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31054 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31055 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31056 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31057 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31058 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31059 and cdleme7 31060. (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 31059 Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 31060. (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 31060 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 31059 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 31053 through cdleme7 31060, 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 31061 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 31062 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 31063 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 31064 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 31065 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 31066 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 31067 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 31068 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 31069 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 31070 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 31071 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31072 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31073 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31074 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31075 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31076 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31077 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31078 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31079 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31080 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31081. (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 31081 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 31071 through cdleme11 31081, 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 31082 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 31083 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 31084 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 30697 to cdleme13 31083. 
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 31085 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 31086 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 31087 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 31088 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 31089 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 31090 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 31091 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 31092 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 31093 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 31094 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 31095 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 31096 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 31097 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 31098 Lemma leading to cdleme17c 31099. (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 31099 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 31100 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 )
    < 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-