HomeHome Metamath Proof Explorer
Theorem List (p. 343 of 357)
< 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-24318)
  Hilbert Space Explorer  Hilbert Space Explorer
(24319-25843)
  Users' Mathboxes  Users' Mathboxes
(25844-35614)
 

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme 34201* Lemma E in [Crawley] p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013.)
 |-  .<_  =  ( le `  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 ) )  ->  E! f  e.  T  (
 f `  P )  =  Q )
 
Theoremcdlemf1 34202* Part of Lemma F in [Crawley] p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  A  /\  U  .<_  W ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  E. q  e.  A  ( P  =/=  q  /\  -.  q  .<_  W 
 /\  U  .<_  ( P 
 .\/  q ) ) )
 
Theoremcdlemf2 34203* Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  ./\  =  ( meet `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  A  /\  U  .<_  W ) )  ->  E. p  e.  A  E. q  e.  A  ( ( -.  p  .<_  W  /\  -.  q  .<_  W )  /\  U  =  ( ( p  .\/  q )  ./\  W ) ) )
 
Theoremcdlemf 34204* Lemma F in [Crawley] p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  A  /\  U  .<_  W ) ) 
 ->  E. f  e.  T  ( R `  f )  =  U )
 
Theoremcdlemfnid 34205* cdlemf 34204 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  A  /\  U  .<_  W ) ) 
 ->  E. f  e.  T  ( ( R `  f )  =  U  /\  f  =/=  (  _I  |`  B ) ) )
 
Theoremcdlemftr3 34206* Special case of cdlemf 34204 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  E. f  e.  T  ( f  =/=  (  _I  |`  B ) 
 /\  ( ( R `
  f )  =/= 
 X  /\  ( R `  f )  =/=  Y  /\  ( R `  f
 )  =/=  Z )
 ) )
 
Theoremcdlemftr2 34207* Special case of cdlemf 34204 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  E. f  e.  T  ( f  =/=  (  _I  |`  B ) 
 /\  ( R `  f )  =/=  X  /\  ( R `  f )  =/=  Y ) )
 
Theoremcdlemftr1 34208* Part of proof of Lemma G of [Crawley] p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h  =/= tr f." (Contributed by NM, 25-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  E. f  e.  T  ( f  =/=  (  _I  |`  B ) 
 /\  ( R `  f )  =/=  X ) )
 
Theoremcdlemftr0 34209* Special case of cdlemf 34204 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  E. f  e.  T  f  =/=  (  _I  |`  B ) )
 
Theoremtrlord 34210* The ordering of two Hilbert lattice elements (under the fiducial hyperplane  W) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) ) 
 ->  ( X  .<_  Y  <->  A. f  e.  T  ( ( R `  f )  .<_  X  ->  ( R `  f ) 
 .<_  Y ) ) )
 
Theoremcdlemg1a 34211* Shorter expression for  G. TODO: fix comment. TODO: shorten using cdleme 34201 or vice-versa? Also, if not shortened with cdleme 34201, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  G  =  ( iota_ f  e.  T  ( f `  P )  =  Q )
 )
 
Theoremcdlemg1b2 34212* This theorem can be used to shorten 
G  = hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  F  =  G )
 
Theoremcdlemg1idlemN 34213* Lemma for cdlemg1idN 34218. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  X  e.  B )  /\  P  =  Q )  ->  ( F `  X )  =  X )
 
Theoremcdlemg1fvawlemN 34214* Lemma for ltrniotafvawN 34219. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 ->  ( ( F `  R )  e.  A  /\  -.  ( F `  R )  .<_  W ) )
 
Theoremcdlemg1ltrnlem 34215* Lemma for ltrniotacl 34220. (Contributed by NM, 18-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  F  e.  T )
 
Theoremcdlemg1finvtrlemN 34216* Lemma for ltrniotacnvN 34221. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  `' F  e.  T )
 
Theoremcdlemg1bOLDN 34217* This theorem can be used to shorten 
F  = hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  F  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) ) )
 
Theoremcdlemg1idN 34218* Version of cdleme31id 34035 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  X  e.  B )  /\  P  =  Q )  ->  ( F `  X )  =  X )
 
TheoremltrniotafvawN 34219* Version of cdleme46fvaw 34142 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 ->  ( ( F `  R )  e.  A  /\  -.  ( F `  R )  .<_  W ) )
 
Theoremltrniotacl 34220* Version of cdleme50ltrn 34198 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  F  e.  T )
 
TheoremltrniotacnvN 34221* Version of cdleme51finvtrN 34199 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  `' F  e.  T )
 
Theoremltrniotaval 34222* Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  ( F `  P )  =  Q )
 
Theoremltrniotacnvval 34223* Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  Q )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 ->  ( `' F `  Q )  =  P )
 
TheoremltrniotaidvalN 34224* Value of the unique translation specified by identity value. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  F  =  ( iota_ f  e.  T  ( f `  P )  =  P )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  F  =  (  _I  |`  B ) )
 
TheoremltrniotavalbN 34225* Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014.) (New usage is discouraged.)
 |-  .<_  =  ( le `  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 )  ->  ( ( F `
  P )  =  Q  <->  F  =  ( iota_
 f  e.  T  ( f `  P )  =  Q ) ) )
 
Theoremcdlemeiota 34226* A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  F  e.  T )  ->  F  =  (
 iota_ f  e.  T  ( f `  P )  =  ( F `  P ) ) )
 
Theoremcdlemg1ci2 34227* Any function of the form of the function constructed for cdleme 34201 is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
 |-  .<_  =  ( le `  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  =  (
 iota_ f  e.  T  ( f `  P )  =  Q )
 )  ->  F  e.  T )
 
Theoremcdlemg1cN 34228* Any translation belongs to the set of functions constructed for cdleme 34201. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  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 `  P )  =  Q )  ->  ( F  e.  T 
 <->  F  =  ( iota_ f  e.  T  ( f `
  P )  =  Q ) ) )
 
Theoremcdlemg1cex 34229* Any translation is one of our  F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 34204? (Contributed by NM, 17-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( F  e.  T  <->  E. p  e.  A  E. q  e.  A  ( -.  p  .<_  W  /\  -.  q  .<_  W  /\  F  =  ( iota_ f  e.  T  ( f `  p )  =  q )
 ) ) )
 
Theoremcdlemg2cN 34230* Any translation belongs to the set of functions constructed for cdleme 34201. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F `  P )  =  Q )  ->  ( F  e.  T  <->  F  =  G ) )
 
Theoremcdlemg2dN 34231* This theorem can be used to shorten 
G  = hypothesis. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  ( iota_ z  e.  B  A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( if ( s 
 .<_  ( P  .\/  Q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  Q ) ) 
 ->  F  =  G )
 
Theoremcdlemg2cex 34232* Any translation is one of our  F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 34204? (Contributed by NM, 22-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( p  .\/  q )  ./\  W )   &    |-  D  =  ( (
 t  .\/  U )  ./\  ( q  .\/  (
 ( p  .\/  t
 )  ./\  W ) ) )   &    |-  E  =  ( ( p  .\/  q
 )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( p  =/=  q  /\  -.  x  .<_  W ) ,  ( iota_
 z  e.  B  A. s  e.  A  (
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( p 
 .\/  q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( p  .\/  q )
 )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( F  e.  T 
 <-> 
 E. p  e.  A  E. q  e.  A  ( -.  p  .<_  W  /\  -.  q  .<_  W  /\  F  =  G ) ) )
 
Theoremcdlemg2ce 34233* Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( p  .\/  q )  ./\  W )   &    |-  D  =  ( (
 t  .\/  U )  ./\  ( q  .\/  (
 ( p  .\/  t
 )  ./\  W ) ) )   &    |-  E  =  ( ( p  .\/  q
 )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( p  =/=  q  /\  -.  x  .<_  W ) ,  ( iota_
 z  e.  B  A. s  e.  A  (
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( p 
 .\/  q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( p  .\/  q )
 )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  ( F  =  G  ->  ( ps  <->  ch ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( p  e.  A  /\  -.  p  .<_  W )  /\  ( q  e.  A  /\  -.  q  .<_  W ) )  /\  ph )  ->  ch )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ph )  ->  ps )
 
Theoremcdlemg2jlemOLDN 34234* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r  \/ s) = f(r)  \/ s, p. 115 10th line from bottom. TODO: Combine with cdlemg2jOLDN 34239? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( p  .\/  q )  ./\  W )   &    |-  D  =  ( (
 t  .\/  U )  ./\  ( q  .\/  (
 ( p  .\/  t
 )  ./\  W ) ) )   &    |-  E  =  ( ( p  .\/  q
 )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( p  =/=  q  /\  -.  x  .<_  W ) ,  ( iota_
 z  e.  B  A. s  e.  A  (
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( p 
 .\/  q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( p  .\/  q )
 )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  F  e.  T )  ->  ( F `  ( P  .\/  Q ) )  =  ( ( F `  P )  .\/  ( F `  Q ) ) )
 
Theoremcdlemg2fvlem 34235* Lemma for cdlemg2fv 34240. (Contributed by NM, 23-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( p  .\/  q )  ./\  W )   &    |-  D  =  ( (
 t  .\/  U )  ./\  ( q  .\/  (
 ( p  .\/  t
 )  ./\  W ) ) )   &    |-  E  =  ( ( p  .\/  q
 )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( p  =/=  q  /\  -.  x  .<_  W ) ,  ( iota_
 z  e.  B  A. s  e.  A  (
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( p 
 .\/  q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( p  .\/  q )
 )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W ) )  /\  ( F  e.  T  /\  ( P  .\/  ( X 
 ./\  W ) )  =  X ) )  ->  ( F `  X )  =  ( ( F `
  P )  .\/  ( X  ./\  W ) ) )
 
Theoremcdlemg2klem 34236* cdleme42keg 34127 with simpler hypotheses. TODO: FIX COMMENT (Contributed by NM, 22-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( p  .\/  q )  ./\  W )   &    |-  D  =  ( (
 t  .\/  U )  ./\  ( q  .\/  (
 ( p  .\/  t
 )  ./\  W ) ) )   &    |-  E  =  ( ( p  .\/  q
 )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  G  =  ( x  e.  B  |->  if ( ( p  =/=  q  /\  -.  x  .<_  W ) ,  ( iota_
 z  e.  B  A. s  e.  A  (
 ( -.  s  .<_  W 
 /\  ( s  .\/  ( x  ./\  W ) )  =  x ) 
 ->  z  =  ( if ( s  .<_  ( p 
 .\/  q ) ,  ( iota_ y  e.  B  A. t  e.  A  ( ( -.  t  .<_  W 
 /\  -.  t  .<_  ( p  .\/  q )
 )  ->  y  =  E ) ) , 
 [_ s  /  t ]_ D )  .\/  ( x  ./\  W ) ) ) ) ,  x ) )   &    |-  V  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  F  e.  T )  ->  ( ( F `
  P )  .\/  ( F `  Q ) )  =  ( ( F `  P ) 
 .\/  V ) )
 
Theoremcdlemg2idN 34237 Version of cdleme31id 34035 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H  /\  F  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( F `  P )  =  Q  /\  X  e.  B )  /\  P  =  Q )  ->  ( F `  X )  =  X )
 
Theoremcdlemg3a 34238 Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p  \/ q = p  \/ u. TODO: reformat cdleme0cp 33855 to match this, then replace with cdleme0cp 33855. (Contributed by NM, 19-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  /\  -.  P  .<_  W )  /\  Q  e.  A )  ->  ( P 
 .\/  Q )  =  ( P  .\/  U )
 )
 
Theoremcdlemg2jOLDN 34239 TODO: Replace this with ltrnj 33773. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  F  e.  T )  ->  ( F `  ( P  .\/  Q ) )  =  ( ( F `  P ) 
 .\/  ( F `  Q ) ) )
 
Theoremcdlemg2fv 34240 Value of a translation in terms of an associated atom. cdleme48fvg 34141 with simpler hypotheses. TODO: Use ltrnj 33773 to vastly simplify. (Contributed by NM, 23-Apr-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( X  e.  B  /\  -.  X  .<_  W ) )  /\  ( F  e.  T  /\  ( P  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( F `
  X )  =  ( ( F `  P )  .\/  ( X 
 ./\  W ) ) )
 
Theoremcdlemg2fv2 34241 Value of a translation in terms of an associated atom. TODO: FIX COMMENT TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 34164 that use more complex proofs? TODO: Use ltrnj 33773 to vastly simplify. (Contributed by NM, 23-Apr-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  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 ) )  /\  F  e.  T )  ->  ( F `  ( R  .\/  U ) )  =  ( ( F `  R )  .\/  U ) )
 
Theoremcdlemg2k 34242 cdleme42keg 34127 with simpler hypotheses. TODO: FIX COMMENT Todo: derive from cdlemg3a 34238, cdlemg2fv2 34241, cdlemg2jOLDN 34239, ltrnel 33780? (Contributed by NM, 22-Apr-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  F  e.  T )  ->  ( ( F `  P ) 
 .\/  ( F `  Q ) )  =  ( ( F `  P )  .\/  U ) )
 
Theoremcdlemg2kq 34243 cdlemg2k 34242 with  P and  Q swapped. TODO: FIX COMMENT (Contributed by NM, 15-May-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  F  e.  T )  ->  ( ( F `  P ) 
 .\/  ( F `  Q ) )  =  ( ( F `  Q )  .\/  U ) )
 
Theoremcdlemg2l 34244 TODO: FIX COMMENT (Contributed by NM, 23-Apr-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  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 ) )  ->  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =  ( ( F `  ( G `  P ) )  .\/  U )
 )
 
Theoremcdlemg2m 34245 TODO: FIX COMMENT T (Contributed by NM, 25-Apr-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  F  e.  T )  ->  ( ( ( F `  P )  .\/  ( F `  Q ) )  ./\  W )  =  U )
 
Theoremcdlemg5 34246* TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 33646? TODO: The  .\/ hypothesis is unused. FIX COMMENT (Contributed by NM, 26-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  E. q  e.  A  ( P  =/=  q  /\  -.  q  .<_  W ) )
 
Theoremcdlemb3 34247* Given two atoms not under the fiducial co-atom  W, there is a third. Lemma B in [Crawley] p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 33646? Then replace cdlemb2 33682 with it. This is a more general version of cdlemb2 33682 without  P  =/=  Q condition. (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( 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 ) ) 
 ->  E. r  e.  A  ( -.  r  .<_  W  /\  -.  r  .<_  ( P  .\/  Q ) ) )
 
Theoremcdlemg7fvbwN 34248 Properties of a translation of an element not under  W. TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 34143? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  B  =  ( Base `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  F  e.  T )  ->  ( ( F `  X )  e.  B  /\  -.  ( F `  X ) 
 .<_  W ) )
 
Theoremcdlemg4a 34249 TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.)
 |-  .<_  =  ( le `  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 `  ( G `  P ) )  =  P ) 
 ->  ( R `  F )  =  ( R `  G ) )
 
Theoremcdlemg4b1 34250 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  G  e.  T )  ->  ( P  .\/  V )  =  ( P  .\/  ( G `  P ) ) )
 
Theoremcdlemg4b2 34251 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  G  e.  T )  ->  ( ( G `  P )  .\/  V )  =  ( P  .\/  ( G `  P ) ) )
 
Theoremcdlemg4b12 34252 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  G  e.  T )  ->  ( ( G `  P )  .\/  V )  =  ( P  .\/  V ) )
 
Theoremcdlemg4c 34253 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  G  e.  T )  /\  -.  Q  .<_  ( P  .\/  V ) )  ->  -.  ( G `  Q )  .<_  ( P  .\/  V )
 )
 
Theoremcdlemg4d 34254 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  -.  ( G `  Q )  .<_  ( ( G `
  P )  .\/  ( F `  ( G `
  P ) ) ) )
 
Theoremcdlemg4e 34255 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   &    |-  ./\  =  ( meet `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  Q ) )  =  ( ( ( G `  Q ) 
 .\/  ( R `  F ) )  ./\  ( ( F `  ( G `  P ) )  .\/  ( (
 ( G `  P )  .\/  ( G `  Q ) )  ./\  W ) ) ) )
 
Theoremcdlemg4f 34256 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   &    |-  ./\  =  ( meet `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  Q ) )  =  ( ( Q 
 .\/  V )  ./\  ( P  .\/  ( ( P 
 .\/  Q )  ./\  W ) ) ) )
 
Theoremcdlemg4g 34257 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   &    |-  ./\  =  ( meet `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  Q ) )  =  ( ( Q 
 .\/  V )  ./\  ( P  .\/  Q ) ) )
 
Theoremcdlemg4 34258 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  Q ) )  =  Q )
 
Theoremcdlemg6a 34259* TODO: FIX COMMENT TODO: replace with cdlemg4 34258. (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( r  e.  A  /\  -.  r  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  r  .<_  ( P  .\/  V )  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  r ) )  =  r )
 
Theoremcdlemg6b 34260* TODO: FIX COMMENT TODO: replace with cdlemg4 34258. (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( r  e.  A  /\  -.  r  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  -.  Q  .<_  ( r  .\/  V )  /\  ( F `
  ( G `  r ) )  =  r ) )  ->  ( F `  ( G `
  Q ) )  =  Q )
 
Theoremcdlemg6c 34261* TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  Q  .<_  ( P  .\/  V )  /\  ( F `  ( G `  P ) )  =  P ) )  ->  ( (
 ( r  e.  A  /\  -.  r  .<_  W ) 
 /\  -.  r  .<_  ( P  .\/  V )
 )  ->  ( F `  ( G `  Q ) )  =  Q ) )
 
Theoremcdlemg6d 34262* TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  Q  .<_  ( P  .\/  V )  /\  ( F `  ( G `  P ) )  =  P ) )  ->  ( (
 ( r  e.  A  /\  -.  r  .<_  W ) 
 /\  -.  r  .<_  ( P  .\/  ( G `  P ) ) ) 
 ->  ( F `  ( G `  Q ) )  =  Q ) )
 
Theoremcdlemg6e 34263 TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  .\/  =  ( join `  K )   &    |-  V  =  ( R `  G )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  F  e.  T )  /\  ( G  e.  T  /\  Q  .<_  ( P  .\/  V )  /\  ( F `  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `  Q ) )  =  Q )
 
Theoremcdlemg6 34264 TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
 |-  .<_  =  ( le `  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  /\  ( F `  ( G `  P ) )  =  P ) ) 
 ->  ( F `  ( G `  Q ) )  =  Q )
 
Theoremcdlemg7fvN 34265 Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( 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 )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  ( P  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  ( F `  ( G `  X ) )  =  ( ( F `
  ( G `  P ) )  .\/  ( X  ./\  W ) ) )
 
Theoremcdlemg7aN 34266 TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  ( F `  ( G `  P ) )  =  P ) ) 
 ->  ( F `  ( G `  X ) )  =  X )
 
Theoremcdlemg7N 34267 TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  /\  ( F  e.  T  /\  G  e.  T  /\  ( F `
  ( G `  P ) )  =  P ) )  ->  ( F `  ( G `
  X ) )  =  X )
 
Theoremcdlemg8a 34268 TODO: FIX COMMENT (Contributed by NM, 29-Apr-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  /\  ( F `  ( G `  P ) )  =  P ) ) 
 ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg8b 34269 TODO: FIX COMMENT (Contributed by NM, 29-Apr-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =  ( P  .\/  Q )  /\  ( F `  ( G `  P ) )  =/=  P ) )  ->  ( P  .\/  ( F `  ( G `  P ) ) )  =  ( P 
 .\/  Q ) )
 
Theoremcdlemg8c 34270 TODO: FIX COMMENT (Contributed by NM, 29-Apr-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =  ( P  .\/  Q )  /\  ( F `  ( G `  P ) )  =/=  P ) )  ->  ( Q  .\/  ( F `  ( G `  Q ) ) )  =  ( P 
 .\/  Q ) )
 
Theoremcdlemg8d 34271 TODO: FIX COMMENT (Contributed by NM, 29-Apr-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =  ( P  .\/  Q )  /\  ( F `  ( G `  P ) )  =/=  P ) )  ->  ( ( P  .\/  ( F `  ( G `  P ) ) )  ./\  W )  =  ( ( Q 
 .\/  ( F `  ( G `  Q ) ) )  ./\  W ) )
 
Theoremcdlemg8 34272 TODO: FIX COMMENT (Contributed by NM, 29-Apr-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  W )  =  ( ( Q  .\/  ( F `  ( G `
  Q ) ) )  ./\  W )
 )
 
Theoremcdlemg9a 34273 TODO: FIX COMMENT (Contributed by NM, 1-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  U )  ./\  ( ( F `  ( G `  P ) )  .\/  U ) )  .<_  ( ( G `  P ) 
 .\/  U ) )
 
Theoremcdlemg9b 34274 The triples  <. P ,  ( F `  ( G `
 P ) ) ,  ( F `  P ) >. and  <. Q , 
( F `  ( G `  Q )
) ,  ( F `
 Q ) >. are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 1-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  =/=  Q  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  Q )  ./\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `
  Q ) ) ) )  .<_  ( ( G `  P ) 
 .\/  ( G `  Q ) ) )
 
Theoremcdlemg9 34275 The triples  <. P ,  ( F `  ( G `
 P ) ) ,  ( F `  P ) >. and  <. Q , 
( F `  ( G `  Q )
) ,  ( F `
 Q ) >. are axially perspective by dalaw 33527. Part of Lemma G of [Crawley] p. 116, last 2 lines. TODO: FIX COMMENT (Contributed by NM, 1-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  =/=  Q  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( ( P  .\/  ( F `  ( G `
  P ) ) )  ./\  ( Q  .\/  ( F `  ( G `  Q ) ) ) )  .<_  ( ( ( ( F `  ( G `  P ) )  .\/  ( G `  P ) )  ./\  ( ( F `  ( G `  Q ) )  .\/  ( G `  Q ) ) ) 
 .\/  ( ( ( G `  P ) 
 .\/  P )  ./\  (
 ( G `  Q )  .\/  Q ) ) ) )
 
Theoremcdlemg10b 34276 TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-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 )  ->  ( ( ( F `  P ) 
 .\/  ( F `  Q ) )  ./\  W )  =  ( ( P  .\/  Q )  ./\ 
 W ) )
 
Theoremcdlemg10bALTN 34277 TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 34245 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( 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 `  P )  .\/  ( F `
  Q ) ) 
 ./\  W )  =  ( ( P  .\/  Q )  ./\  W ) )
 
Theoremcdlemg11a 34278 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 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( F  e.  T  /\  G  e.  T  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( F `  ( G `
  P ) )  =/=  P )
 
Theoremcdlemg11aq 34279 TODO: FIX COMMENT TODO: can proof using this be restructured to use cdlemg11a 34278? (Contributed by NM, 4-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  /\  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `  Q ) ) )  =/=  ( P  .\/  Q ) ) )  ->  ( F `  ( G `
  Q ) )  =/=  Q )
 
Theoremcdlemg10c 34280 TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in trl* area? (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 ) )  ->  ( ( R `  F ) 
 .<_  ( ( G `  P )  .\/  ( G `
  Q ) )  <-> 
 ( R `  F )  .<_  ( P  .\/  Q ) ) )
 
Theoremcdlemg10a 34281 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 34282 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 34283 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 34284 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 34285 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 34286 The triples  <. P ,  ( F `  P ) ,  ( F `  ( G `  P ) ) >. and  <. Q , 
( F `  Q
) ,  ( F `
 ( G `  Q ) ) >. are axially perspective by dalaw 33527. 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 34287 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 34288 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 34289 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 34290 TODO: FIX COMMENT TODO: Combine with cdlemg12f 34289. (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 34291 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 34292 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 34293 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 34294 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 34295 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 34296 Eliminate the  ( F `  P )  =/=  P condition from cdlemg13 34293. 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 34297 Eliminate the  ( ( F `  ( G `  P ) )  .\/  ( F `  ( G `
 Q ) ) )  =/=  ( P 
.\/  Q ) condition from cdlemg13 34293. TODO: FIX COMMENT (Contributed by NM, 25-May-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( (