HomeHome Metamath Proof Explorer
Theorem List (p. 300 of 314)
< 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-21458)
  Hilbert Space Explorer  Hilbert Space Explorer
(21459-22981)
  Users' Mathboxes  Users' Mathboxes
(22982-31321)
 

Theorem List for Metamath Proof Explorer - 29901-30000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme50rn 29901* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  ran  F  =  B )
 
Theoremcdleme50f1o 29902* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  F : B
 -1-1-onto-> B )
 
Theoremcdleme50laut 29903* Part of proof of Lemma D in [Crawley] p. 113.  F is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-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 ) ) )   &    |-  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 ) )   &    |-  I  =  (
 LAut `  K )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  F  e.  I )
 
Theoremcdleme50ldil 29904* Part of proof of Lemma D in [Crawley] p. 113.  F is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-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 ) ) )   &    |-  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 ) )   &    |-  C  =  ( ( LDil `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  F  e.  C )
 
Theoremcdleme50trn1 29905* Part of proof that  F is a tranlation.  -.  R  .<_  ( P  .\/  Q ) case. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( ( R  .\/  ( F `  R ) )  ./\  W )  =  U )
 
Theoremcdleme50trn2a 29906* Part of proof that  F is a translation.  R  .<_  ( P 
.\/  Q ) case. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( R 
 .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )
 ) )  ->  (
 ( R  .\/  ( F `  R ) ) 
 ./\  W )  =  U )
 
Theoremcdleme50trn2 29907* Part of proof that  F is a translation. Remove  S hypotheses no longer needed from cdleme50trn2a 29906. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  R  .<_  ( P 
 .\/  Q ) )  ->  ( ( R  .\/  ( F `  R ) )  ./\  W )  =  U )
 
Theoremcdleme50trn12 29908* Part of proof that  F is a translation. Combine  R  .<_  ( P 
.\/  Q ) and  -.  R  .<_  ( P  .\/  Q ) cases. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  ( ( R  .\/  ( F `  R ) )  ./\  W )  =  U )
 
Theoremcdleme50trn3 29909* Part of proof that  F is a translation.  P  =  Q case. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) )  ->  (
 ( R  .\/  ( F `  R ) ) 
 ./\  W )  =  U )
 
Theoremcdleme50trn123 29910* Part of proof that  F is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 ->  ( ( R  .\/  ( F `  R ) )  ./\  W )  =  U )
 
Theoremcdleme51finvfvN 29911* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-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  =  ( 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  =  ( ( Q  .\/  P )  ./\  W )   &    |-  N  =  ( ( v  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  v )  ./\  W ) ) )   &    |-  O  =  ( ( Q  .\/  P )  ./\  ( N  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  G  =  ( a  e.  B  |->  if ( ( Q  =/=  P 
 /\  -.  a  .<_  W ) ,  ( iota_ c  e.  B A. u  e.  A  ( ( -.  u  .<_  W  /\  ( u  .\/  ( a  ./\  W ) )  =  a )  ->  c  =  ( if ( u  .<_  ( Q  .\/  P ) ,  ( iota_ b  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( Q  .\/  P ) )  ->  b  =  O ) ) , 
 [_ u  /  v ]_ N )  .\/  (
 a  ./\  W ) ) ) ) ,  a
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  X  e.  B )  ->  ( `' F `  X )  =  ( G `  X ) )
 
Theoremcdleme51finvN 29912* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-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  =  ( 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  =  ( ( Q  .\/  P )  ./\  W )   &    |-  N  =  ( ( v  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  v )  ./\  W ) ) )   &    |-  O  =  ( ( Q  .\/  P )  ./\  ( N  .\/  ( ( u  .\/  v )  ./\  W ) ) )   &    |-  G  =  ( a  e.  B  |->  if ( ( Q  =/=  P 
 /\  -.  a  .<_  W ) ,  ( iota_ c  e.  B A. u  e.  A  ( ( -.  u  .<_  W  /\  ( u  .\/  ( a  ./\  W ) )  =  a )  ->  c  =  ( if ( u  .<_  ( Q  .\/  P ) ,  ( iota_ b  e.  B A. v  e.  A  ( ( -.  v  .<_  W  /\  -.  v  .<_  ( Q  .\/  P ) )  ->  b  =  O ) ) , 
 [_ u  /  v ]_ N )  .\/  (
 a  ./\  W ) ) ) ) ,  a
 ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  `' F  =  G )
 
Theoremcdleme50ltrn 29913* Part of proof of Lemma E in [Crawley] p. 113.  F is a lattice translation. TODO: fix comment. (Contributed by NM, 10-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 ) ) )   &    |-  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 ) )   &    |-  T  =  ( ( LTrn `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  F  e.  T )
 
Theoremcdleme51finvtrN 29914* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-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  =  ( 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 ) )  ->  `' F  e.  T )
 
Theoremcdleme50ex 29915* Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (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 )
 
Theoremcdleme 29916* 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 29917* 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 29918* 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 29919* 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 29920* cdlemf 29919 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 29921* Special case of cdlemf 29919 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 29922* Special case of cdlemf 29919 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 29923* 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 29924* Special case of cdlemf 29919 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 29925* 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 29926* Shorter expression for  G. TODO: fix comment. TODO: shorten using cdleme 29916 or vice-versa? Also, if not shortened with cdleme 29916, 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 29927* 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 29928* Lemma for cdlemg1idN 29933. (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 29929* Lemma for ltrniotafvawN 29934. (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 29930* Lemma for ltrniotacl 29935. (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 29931* Lemma for ltrniotacnvN 29936. (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 29932* 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 29933* Version of cdleme31id 29750 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 29934* Version of cdleme46fvaw 29857 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 29935* Version of cdleme50ltrn 29913 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 29936* Version of cdleme51finvtrN 29914 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 29937* 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 29938* 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 29939* 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 29940* 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 29941* 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 29942* Any function of the form of the function constructed for cdleme 29916 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 29943* Any translation belongs to the set of functions constructed for cdleme 29916. 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 29944* Any translation is one of our  F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 29919? (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 29945* Any translation belongs to the set of functions constructed for cdleme 29916. 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 29946* 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 29947* Any translation is one of our  F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 29919? (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 29948* 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 29949* 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 29954? (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 29950* Lemma for cdlemg2fv 29955. (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 29951* cdleme42keg 29842 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 29952 Version of cdleme31id 29750 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 29953 Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p  \/ q = p  \/ u. TODO: reformat cdleme0cp 29570 to match this, then replace with cdleme0cp 29570. (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 29954 TODO: Replace this with ltrnj 29488. (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 29955 Value of a translation in terms of an associated atom. cdleme48fvg 29856 with simpler hypotheses. TODO: Use ltrnj 29488 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 29956 Value of a translation in terms of an associated atom. TODO: FIX COMMENT TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 29879 that use more complex proofs? TODO: Use ltrnj 29488 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 29957 cdleme42keg 29842 with simpler hypotheses. TODO: FIX COMMENT Todo: derive from cdlemg3a 29953, cdlemg2fv2 29956, cdlemg2jOLDN 29954, ltrnel 29495? (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 29958 cdlemg2k 29957 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 29959 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 29960 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 29961* TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 29361? 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 29962* 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 29361? Then replace cdlemb2 29397 with it. This is a more general version of cdlemb2 29397 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 29963 Properties of a translation of an element not under  W. TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 29858? 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 29964 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 29965 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 29966 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 29967 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 29968 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 29969 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 29970 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 29971 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 29972 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 29973 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 29974* TODO: FIX COMMENT TODO: replace with cdlemg4 29973. (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 29975* TODO: FIX COMMENT TODO: replace with cdlemg4 29973. (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 29976* 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 29977* 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 29978 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 29979 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 29980 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 29981 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 29982 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 29983 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 29984 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 29985 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 29986 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 29987 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 29988 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 ) )