HomeHome Metamath Proof Explorer
Theorem List (p. 343 of 406)
< 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-26564)
  Hilbert Space Explorer  Hilbert Space Explorer
(26565-28087)
  Users' Mathboxes  Users' Mathboxes
(28088-40527)
 

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemg10a 34201 TODO: FIX COMMENT. (Contributed by NM, 3-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( P  .\/  ( F `  ( G `  P ) ) ) 
 ./\  ( Q  .\/  ( F `  ( G `
  Q ) ) ) )  .<_  ( ( R `  F ) 
 .\/  ( R `  G ) ) )
 
Theoremcdlemg10 34202 TODO: FIX COMMENT. (Contributed by NM, 4-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( P  .\/  ( F `  ( G `  P ) ) ) 
 ./\  ( Q  .\/  ( F `  ( G `
  Q ) ) ) )  .<_  W )
 
Theoremcdlemg11b 34203 TODO: FIX COMMENT. (Contributed by NM, 5-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A )  /\  ( G  e.  T  /\  P  =/=  Q  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 ) )  ->  ( P  .\/  Q )  =/=  ( ( G `  P )  .\/  ( G `
  Q ) ) )
 
Theoremcdlemg12a 34204 TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  F  e.  T )  /\  ( G  e.  T  /\  P  =/=  Q  /\  ( P  .\/  U )  =/=  ( ( G `
  P )  .\/  U ) ) )  ->  ( ( P  .\/  U )  ./\  ( ( G `  P )  .\/  U ) )  .<_  ( ( F `  ( G `
  P ) ) 
 .\/  U ) )
 
Theoremcdlemg12b 34205 The triples  <. P ,  ( F `  P ) ,  ( F `  ( G `  P ) ) >. and  <. Q , 
( F `  Q
) ,  ( F `
 ( G `  Q ) ) >. are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 5-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  P  =/=  Q  /\  -.  ( R `  G )  .<_  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  Q )  ./\  ( ( G `  P )  .\/  ( G `  Q ) ) )  .<_  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) ) )
 
Theoremcdlemg12c 34206 The triples  <. P ,  ( F `  P ) ,  ( F `  ( G `  P ) ) >. and  <. Q , 
( F `  Q
) ,  ( F `
 ( G `  Q ) ) >. are axially perspective by dalaw 33445. TODO: FIX COMMENT. (Contributed by NM, 5-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  P  =/=  Q  /\  -.  ( R `  G )  .<_  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( G `  P ) )  ./\  ( Q  .\/  ( G `  Q ) ) )  .<_  ( ( ( ( G `
  P )  .\/  ( F `  ( G `
  P ) ) )  ./\  ( ( G `  Q )  .\/  ( F `  ( G `
  Q ) ) ) )  .\/  (
 ( ( F `  ( G `  P ) )  .\/  P )  ./\  ( ( F `  ( G `  Q ) )  .\/  Q )
 ) ) )
 
Theoremcdlemg12d 34207 TODO: FIX COMMENT. (Contributed by NM, 5-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  =/=  Q 
 /\  -.  ( R `  F )  .<_  ( P 
 .\/  Q )  /\  -.  ( R `  G ) 
 .<_  ( P  .\/  Q ) ) )  ->  ( R `  G ) 
 .<_  ( ( R `  F )  .\/  ( ( ( F `  ( G `  P ) ) 
 .\/  P )  ./\  (
 ( F `  ( G `  Q ) ) 
 .\/  Q ) ) ) )
 
Theoremcdlemg12e 34208 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .0.  =  ( 0. `  K )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q )  /\  ( -.  ( R `  F )  .<_  ( P 
 .\/  Q )  /\  -.  ( R `  G ) 
 .<_  ( P  .\/  Q )  /\  ( R `  F )  =/=  ( R `  G ) ) )  ->  ( (
 ( F `  ( G `  P ) ) 
 .\/  P )  ./\  (
 ( F `  ( G `  Q ) ) 
 .\/  Q ) )  =/= 
 .0.  )
 
Theoremcdlemg12f 34209 TODO: FIX COMMENT. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 )  /\  ( R `  F )  =/=  ( R `  G )  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  .<_  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W ) )
 
Theoremcdlemg12g 34210 TODO: FIX COMMENT. TODO: Combine with cdlemg12f 34209. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 )  /\  ( R `  F )  =/=  ( R `  G )  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  =  ( ( P  .\/  ( F `  ( G `  P ) ) ) 
 ./\  W ) )
 
Theoremcdlemg12 34211 TODO: FIX COMMENT. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 )  /\  ( R `  F )  =/=  ( R `  G )  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg13a 34212 TODO: FIX COMMENT. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  ( ( F `
  P )  =/= 
 P  /\  ( R `  F )  =  ( R `  G ) 
 /\  ( ( F `
  ( G `  P ) )  .\/  ( F `  ( G `
  Q ) ) )  =/=  ( P 
 .\/  Q ) ) ) 
 ->  ( P  .\/  ( F `  ( G `  P ) ) )  =  ( ( G `
  P )  .\/  ( F `  ( G `
  P ) ) ) )
 
Theoremcdlemg13 34213 TODO: FIX COMMENT. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  ( ( F `
  P )  =/= 
 P  /\  ( R `  F )  =  ( R `  G ) 
 /\  ( ( F `
  ( G `  P ) )  .\/  ( F `  ( G `
  Q ) ) )  =/=  ( P 
 .\/  Q ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg14f 34214 TODO: FIX COMMENT. (Contributed by NM, 6-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  ( F `  P )  =  P )
 )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg14g 34215 TODO: FIX COMMENT. (Contributed by NM, 22-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  ( G `  P )  =  P )
 )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg15a 34216 Eliminate the  ( F `  P )  =/=  P condition from cdlemg13 34213. TODO: FIX COMMENT. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  ( ( R `
  F )  =  ( R `  G )  /\  ( ( F `
  ( G `  P ) )  .\/  ( F `  ( G `
  Q ) ) )  =/=  ( P 
 .\/  Q ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg15 34217 Eliminate the  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `
 Q ) ) )  =/=  ( P 
.\/  Q ) condition from cdlemg13 34213. TODO: FIX COMMENT. (Contributed by NM, 25-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg16 34218 Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 34202 "implies (2)" (of p. 116). No details are provided by the authors, so there may be a shorter proof; but ours requires the 14 lemmas, one using Desargues' law dalaw 33445, in order to make this inference. This final step eliminates the  ( R `  F )  =/=  ( R `  G ) condition from cdlemg12 34211. TODO: FIX COMMENT. TODO: should we also eliminate  P  =/=  Q here (or earlier)? Do it if we don't need to add it in for something else later. (Contributed by NM, 6-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  (
 ( F `  ( G `  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg16ALTN 34219 This version of cdlemg16 34218 uses cdlemg15a 34216 instead of cdlemg15 34217, in case cdlemg15 34217 ends up not being needed. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  G  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  P  =/=  Q )  /\  ( ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( P  .\/  ( F `  ( G `  P ) ) ) 
 ./\  W )  =  ( ( Q  .\/  ( F `  ( G `  Q ) ) ) 
 ./\  W ) )
 
Theoremcdlemg16z 34220 Eliminate  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `
 Q ) ) )  =/=  ( P 
.\/  Q ) condition from cdlemg16 34218. TODO: would it help to also eliminate  P  =/=  Q here or later? (Contributed by NM, 25-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( -.  ( R `  F )  .<_  ( P  .\/  Q )  /\  -.  ( R `  G )  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg16zz 34221 Eliminate  P  =/=  Q from cdlemg16z 34220. TODO: Use this only if needed. (Contributed by NM, 26-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  ( R `  F )  .<_  ( P 
 .\/  Q )  /\  -.  ( R `  G ) 
 .<_  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg17a 34222 TODO: FIX COMMENT. (Contributed by NM, 8-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( G  e.  T  /\  ( R `  G )  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( G `  P )  .<_  ( P  .\/  Q ) )
 
Theoremcdlemg17b 34223* Part of proof of Lemma G in [Crawley] p. 117, 4th line. Whenever (in their terminology) p  \/ q/0 (i.e. the sublattice from 0 to p  \/ q) contains precisely three atoms and g is not the identity, g(p) = q. See also comments under cdleme0nex 33850. (Contributed by NM, 8-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( G  e.  T  /\  P  =/=  Q )  /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  P )  =  Q )
 
Theoremcdlemg17dN 34224* TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  G  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  P  =/=  Q )  /\  ( ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) )  /\  ( G `  P )  =/=  P ) ) 
 ->  ( R `  G )  =  ( ( P  .\/  Q )  ./\  W ) )
 
Theoremcdlemg17dALTN 34225 Same as cdlemg17dN 34224 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  G  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( ( R `
  G )  .<_  ( P  .\/  Q )  /\  ( G `  P )  =/=  P ) ) 
 ->  ( R `  G )  =  ( ( P  .\/  Q )  ./\  W ) )
 
Theoremcdlemg17e 34226* TODO: fix comment. (Contributed by NM, 8-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( F `  P )  .\/  ( F `  Q ) )  =  ( ( F `  P ) 
 .\/  ( R `  G ) ) )
 
Theoremcdlemg17f 34227* TODO: fix comment. (Contributed by NM, 8-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( F `  P )  .\/  ( F `  Q ) )  =  ( ( F `  P ) 
 .\/  ( G `  ( F `  P ) ) ) )
 
Theoremcdlemg17g 34228* TODO: fix comment. (Contributed by NM, 9-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  ( F `  P ) )  .<_  ( ( F `  P ) 
 .\/  ( F `  Q ) ) )
 
Theoremcdlemg17h 34229* TODO: fix comment. (Contributed by NM, 10-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( F  e.  T  /\  G  e.  T ) 
 /\  ( P  =/=  Q 
 /\  S  .<_  ( ( F `  P ) 
 .\/  ( F `  Q ) ) ) )  /\  ( ( G `  P )  =/=  P  /\  ( R `  G )  .<_  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  ( S  =  ( F `  P )  \/  S  =  ( F `  Q ) ) )
 
Theoremcdlemg17i 34230* TODO: fix comment. (Contributed by NM, 10-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  ( F `  P ) )  =  ( F `  Q ) )
 
Theoremcdlemg17ir 34231* TODO: fix comment. (Contributed by NM, 13-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( F `  ( G `  P ) )  =  ( F `  Q ) )
 
Theoremcdlemg17j 34232* TODO: fix comment. (Contributed by NM, 11-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  ( F `  P ) )  =  ( F `  ( G `  P ) ) )
 
Theoremcdlemg17pq 34233* Utility theorem for swapping  P and  Q. TODO: fix comment. (Contributed by NM, 11-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( (
 ( K  e.  HL  /\  W  e.  H ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  Q  =/=  P ) 
 /\  ( ( G `
  Q )  =/= 
 Q  /\  ( R `  G )  .<_  ( Q 
 .\/  P )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( Q  .\/  r )  =  ( P  .\/  r ) ) ) ) )
 
Theoremcdlemg17bq 34234* cdlemg17b 34223 with  P and  Q swapped. Antecedent  F  e.  ( T `  W ) is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 34223 also? (Contributed by NM, 13-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  Q )  =  P )
 
Theoremcdlemg17iqN 34235* cdlemg17i 34230 with  P and  Q swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( 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  /\  G  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  P  =/=  Q )  /\  ( ( R `
  G )  .<_  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) )  /\  ( G `  P )  =/= 
 P ) )  ->  ( G `  ( F `
  Q ) )  =  ( F `  P ) )
 
Theoremcdlemg17irq 34236* cdlemg17ir 34231 with  P and  Q swapped. (Contributed by NM, 13-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( F `  ( G `  Q ) )  =  ( F `  P ) )
 
Theoremcdlemg17jq 34237* cdlemg17j 34232 with  P and  Q swapped. (Contributed by NM, 13-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  ( F `  Q ) )  =  ( F `  ( G `  Q ) ) )
 
Theoremcdlemg17 34238* Part of Lemma G of [Crawley] p. 117, lines 7 and 8. We show an argument whose value at  G equals itself. TODO: fix comment. (Contributed by NM, 12-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( G `
  P )  =/= 
 P  /\  ( R `  G )  .<_  ( P 
 .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( G `  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) ) )  =  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) ) )
 
Theoremcdlemg18a 34239 Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-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 )  /\  ( P  e.  A  /\  Q  e.  A  /\  F  e.  T )  /\  ( P  =/=  Q  /\  ( ( F `  Q )  .\/  ( F `
  P ) )  =/=  ( P  .\/  Q ) ) )  ->  ( P  .\/  ( F `
  Q ) )  =/=  ( Q  .\/  ( F `  P ) ) )
 
Theoremcdlemg18b 34240 Lemma for cdlemg18c 34241. TODO: fix comment. (Contributed by NM, 15-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  F  e.  T )  /\  ( P  =/=  Q 
 /\  ( F `  P )  =/=  Q  /\  ( ( F `  Q )  .\/  ( F `
  P ) )  =/=  ( P  .\/  Q ) ) )  ->  -.  P  .<_  ( U  .\/  ( F `  Q ) ) )
 
Theoremcdlemg18c 34241 Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  F  e.  T )  /\  ( P  =/=  Q 
 /\  ( F `  P )  =/=  Q  /\  ( ( F `  Q )  .\/  ( F `
  P ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  Q ) )  ./\  ( Q  .\/  ( F `  P ) ) )  e.  A )
 
Theoremcdlemg18d 34242* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q  /\  ( G `
  P )  =/= 
 P )  /\  (
 ( R `  G )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  e.  A )
 
Theoremcdlemg18 34243* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q  /\  ( G `
  P )  =/= 
 P )  /\  (
 ( R `  G )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  .<_  W )
 
Theoremcdlemg19a 34244* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q  /\  ( G `
  P )  =/= 
 P )  /\  (
 ( R `  G )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  =  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )
 )
 
Theoremcdlemg19 34245* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q  /\  ( G `
  P )  =/= 
 P )  /\  (
 ( R `  G )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg20 34246* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 23-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( R `
  G )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg21 34247* Version of cdlemg19 with  ( R `  F
)  .<_  ( P  .\/  Q ) instead of  ( R `  G )  .<_  ( P 
.\/  Q ) as a condition. (Contributed by NM, 23-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q  /\  ( F `
  P )  =/= 
 P )  /\  (
 ( R `  F )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg22 34248* cdlemg21 34247 with  ( F `  P )  =/=  P condition removed. (Contributed by NM, 23-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( R `
  F )  .<_  ( P  .\/  Q )  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -.  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg24 34249* Combine cdlemg16z 34220 and cdlemg22 34248. TODO: Fix comment. (Contributed by NM, 24-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( ( F `  ( G `
  P ) ) 
 .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q )  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg37 34250* Use cdlemg8 34192 to eliminate the  =/=  ( P  .\/  Q
) condition of cdlemg24 34249. (Contributed by NM, 31-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  P  =/=  Q  /\  -. 
 E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg25zz 34251 cdlemg16zz 34221 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( z  e.  A  /\  -.  z  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  ( R `  F )  .<_  ( P 
 .\/  z )  /\  -.  ( R `  G )  .<_  ( P  .\/  z ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( z  .\/  ( F `  ( G `
  z ) ) )  ./\  W )
 )
 
Theoremcdlemg26zz 34252 cdlemg16zz 34221 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-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 )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( z  e.  A  /\  -.  z  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  ( R `  F )  .<_  ( Q 
 .\/  z )  /\  -.  ( R `  G )  .<_  ( Q  .\/  z ) ) ) 
 ->  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )  =  ( ( z  .\/  ( F `  ( G `
  z ) ) )  ./\  W )
 )
 
Theoremcdlemg27a 34253 For use with case when  ( P  .\/  v
)  ./\  ( Q  .\/  ( R `  F
) ) or  ( P  .\/  v )  ./\  ( Q  .\/  ( R `  F ) ) is zero, letting us establish  -.  z  .<_  W  /\  z  .<_  ( P 
.\/  v ) via 4atex 33635. TODO: Fix comment. (Contributed by NM, 28-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( v  e.  A  /\  v  .<_  W ) )  /\  ( z  e.  A  /\  F  e.  T ) 
 /\  ( v  =/=  ( R `  F )  /\  z  .<_  ( P 
 .\/  v )  /\  ( F `  P )  =/=  P ) ) 
 ->  -.  ( R `  F )  .<_  ( P 
 .\/  z ) )
 
Theoremcdlemg28a 34254 Part of proof of Lemma G of [Crawley] p. 116. First equality of the equation of line 14 on p. 117. (Contributed by NM, 29-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( v  e.  A  /\  v  .<_  W ) )  /\  ( ( z  e.  A  /\  -.  z  .<_  W )  /\  F  e.  T  /\  G  e.  T )  /\  ( ( v  =/=  ( R `
  F )  /\  v  =/=  ( R `  G ) )  /\  z  .<_  ( P  .\/  v )  /\  ( ( F `  P )  =/=  P  /\  ( G `  P )  =/= 
 P ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( z  .\/  ( F `  ( G `
  z ) ) )  ./\  W )
 )
 
Theoremcdlemg31b0N 34255 TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  F  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( v  e.  A  /\  v  .<_  W )  /\  v  =/=  ( R `  F )  /\  ( F `
  P )  =/= 
 P ) )  ->  ( N  e.  A  \/  N  =  ( 0. `  K ) ) )
 
Theoremcdlemg31b0a 34256 TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( v  e.  A  /\  v  .<_  W ) )  /\  ( F  e.  T  /\  v  =/=  ( R `  F ) ) )  ->  ( N  e.  A  \/  N  =  ( 0. `  K ) ) )
 
Theoremcdlemg27b 34257 TODO: Fix comment. (Contributed by NM, 28-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 z  e.  A  /\  ( v  e.  A  /\  v  .<_  W ) 
 /\  ( F  e.  T  /\  z  =/=  N ) )  /\  ( v  =/=  ( R `  F )  /\  z  .<_  ( P  .\/  v )  /\  ( F `  P )  =/=  P ) ) 
 ->  -.  ( R `  F )  .<_  ( Q 
 .\/  z ) )
 
Theoremcdlemg31a 34258 TODO: fix comment. (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A )  /\  ( v  e.  A  /\  F  e.  T ) )  ->  N  .<_  ( P  .\/  v )
 )
 
Theoremcdlemg31b 34259 TODO: fix comment. (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A )  /\  ( v  e.  A  /\  F  e.  T ) )  ->  N  .<_  ( Q  .\/  ( R `  F ) ) )
 
Theoremcdlemg31c 34260 Show that when  N is an atom, it is not under  W. TODO: Is there a shorter direct proof? TODO: should we eliminate  ( F `  P )  =/=  P here? (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  F  e.  T )  /\  ( v  =/=  ( R `  F )  /\  ( F `  P )  =/=  P  /\  N  e.  A )
 )  ->  -.  N  .<_  W )
 
Theoremcdlemg31d 34261 Eliminate  ( F `  P )  =/=  P from cdlemg31c 34260. TODO: Prove directly. TODO: do we need to eliminate  ( F `  P )  =/=  P? It might be better to do this all at once at the end. See also cdlemg29 34266 vs. cdlemg28 34265. (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( v  e.  A  /\  v  .<_  W ) )  /\  ( F  e.  T  /\  v  =/=  ( R `  F )  /\  N  e.  A )
 )  ->  -.  N  .<_  W )
 
Theoremcdlemg33b0 34262* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  N  e.  A  /\  F  e.  T ) 
 /\  ( P  =/=  Q 
 /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33c0 34263* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  F  e.  T )  /\  ( P  =/=  Q 
 /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  E. z  e.  A  ( -.  z  .<_  W  /\  z  .<_  ( P  .\/  v )
 ) )
 
Theoremcdlemg28b 34264* Part of proof of Lemma G of [Crawley] p. 116. Second equality of the equation of line 14 on p. 117. Note that  -.  z  .<_  W is redundant here (but simplifies cdlemg28 34265.) (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( z  e.  A  /\  -.  z  .<_  W )  /\  ( F  e.  T  /\  G  e.  T )
 )  /\  ( (
 z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) )  /\  (
 v  =/=  ( R `  F )  /\  v  =/=  ( R `  G ) )  /\  ( ( F `  P )  =/=  P  /\  ( G `  P )  =/= 
 P ) ) ) 
 ->  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )  =  ( ( z  .\/  ( F `  ( G `
  z ) ) )  ./\  W )
 )
 
Theoremcdlemg28 34265* Part of proof of Lemma G of [Crawley] p. 116. Chain the equalities of line 14 on p. 117. TODO: rearrange hypotheses in the order of cdlemg29 34266 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( z  e.  A  /\  -.  z  .<_  W )  /\  ( F  e.  T  /\  G  e.  T )
 )  /\  ( (
 z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) )  /\  (
 v  =/=  ( R `  F )  /\  v  =/=  ( R `  G ) )  /\  ( ( F `  P )  =/=  P  /\  ( G `  P )  =/= 
 P ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg29 34266* Eliminate  ( F `  P )  =/=  P and  ( G `  P )  =/=  P from cdlemg28 34265. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( z  e.  A  /\  -.  z  .<_  W )  /\  ( F  e.  T  /\  G  e.  T )
 )  /\  ( (
 z  =/=  N  /\  z  =/=  O )  /\  z  .<_  ( P  .\/  v )  /\  ( v  =/=  ( R `  F )  /\  v  =/=  ( R `  G ) ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg33a 34267* TODO: Fix comment. (Contributed by NM, 29-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( N  e.  A  /\  O  e.  A )  /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( ( P  =/=  Q  /\  N  =/=  O )  /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33b 34268* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( N  e.  A  /\  O  e.  A )  /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( P  =/=  Q  /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33c 34269* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( N  e.  A  /\  O  =  ( 0. `  K ) )  /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( P  =/=  Q  /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33d 34270* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( N  =  ( 0. `  K ) 
 /\  O  e.  A )  /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( P  =/=  Q  /\  v  =/=  ( R `  G )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33e 34271* TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( N  =  ( 0. `  K ) 
 /\  O  =  ( 0. `  K ) )  /\  ( F  e.  T  /\  G  e.  T ) )  /\  ( P  =/=  Q  /\  v  =/=  ( R `  F )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v
 ) ) ) )
 
Theoremcdlemg33 34272* Combine cdlemg33b 34268, cdlemg33c 34269, cdlemg33d 34270, cdlemg33e 34271. TODO: Fix comment. (Contributed by NM, 30-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q )  /\  ( v  =/=  ( R `  F )  /\  v  =/=  ( R `  G )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  E. z  e.  A  ( -.  z  .<_  W  /\  ( z  =/=  N  /\  z  =/=  O  /\  z  .<_  ( P  .\/  v )
 ) ) )
 
Theoremcdlemg34 34273* Use cdlemg33 to eliminate  z from cdlemg29 34266. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  N  =  ( ( P  .\/  v )  ./\  ( Q 
 .\/  ( R `  F ) ) )   &    |-  O  =  ( ( P  .\/  v )  ./\  ( Q  .\/  ( R `
  G ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( v  e.  A  /\  v  .<_  W ) 
 /\  ( F  e.  T  /\  G  e.  T )  /\  P  =/=  Q )  /\  ( v  =/=  ( R `  F )  /\  v  =/=  ( R `  G )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg35 34274* TODO: Fix comment. TODO: should we have a more general version of hlsupr 32945 to avoid the  =/= conditions? (Contributed by NM, 31-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  F  e.  T  /\  G  e.  T )  /\  ( ( F `
  P )  =/= 
 P  /\  ( G `  P )  =/=  P  /\  ( R `  F )  =/=  ( R `  G ) ) ) 
 ->  E. v  e.  A  ( v  .<_  W  /\  ( v  =/=  ( R `  F )  /\  v  =/=  ( R `  G ) ) ) )
 
Theoremcdlemg36 34275* Use cdlemg35 to eliminate  v from cdlemg34 34273. TODO: Fix comment. (Contributed by NM, 31-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( ( F `  P )  =/=  P  /\  ( G `  P )  =/= 
 P )  /\  ( R `  F )  =/=  ( R `  G )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) ) ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg38 34276 Use cdlemg37 34250 to eliminate  E. r  e.  A from cdlemg36 34275. TODO: Fix comment. (Contributed by NM, 31-May-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 ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) 
 /\  ( ( ( F `  P )  =/=  P  /\  ( G `  P )  =/= 
 P )  /\  ( R `  F )  =/=  ( R `  G ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg39 34277 Eliminate  =/= conditions from cdlemg38 34276. TODO: Would this better be done at cdlemg35 34274? TODO: Fix comment. (Contributed by NM, 31-May-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 )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  P  =/=  Q ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg40 34278 Eliminate  P  =/=  Q conditions from cdlemg39 34277. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg41 34279 Convert cdlemg40 34278 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T ) )  ->  ( ( P  .\/  ( ( F  o.  G ) `  P ) )  ./\  W )  =  ( ( Q  .\/  ( ( F  o.  G ) `  Q ) )  ./\  W ) )
 
Theoremltrnco 34280 The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  ->  ( F  o.  G )  e.  T )
 
Theoremtrlcocnv 34281 Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  ->  ( R `  ( F  o.  `' G ) )  =  ( R `
  ( G  o.  `' F ) ) )
 
Theoremtrlcoabs 34282 Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( ( F  o.  G ) `  P )  .\/  ( R `  F ) )  =  ( ( G `  P )  .\/  ( R `
  F ) ) )
 
Theoremtrlcoabs2N 34283 Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( F `  P )  .\/  ( R `  ( G  o.