HomeHome Metamath Proof Explorer
Theorem List (p. 315 of 325)
< 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-22374)
  Hilbert Space Explorer  Hilbert Space Explorer
(22375-23897)
  Users' Mathboxes  Users' Mathboxes
(23898-32447)
 

Theorem List for Metamath Proof Explorer - 31401-31500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemk40f 31401* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)
 |-  X  =  ( iota_ z  e.  T ph )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X ) )   =>    |-  ( ( F  =/=  N 
 /\  G  e.  T )  ->  ( U `  G )  =  [_ G  /  g ]_ X )
 
Theoremcdlemk41 31402* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.)
 |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   =>    |-  ( G  e.  T  -> 
 [_ G  /  g ]_ Y  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( Z  .\/  ( R `  ( G  o.  `' b ) ) ) ) )
 
Theoremcdlemkfid1N 31403 Lemma for cdlemkfid3N 31407. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  G  e.  T )  /\  (
 ( R `  G )  =/=  ( R `  F )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( P  .\/  ( R `  G ) )  ./\  ( ( F `  P )  .\/  ( R `
  ( G  o.  `' F ) ) ) )  =  ( G `
  P ) )
 
Theoremcdlemkid1 31404 Lemma for cdlemkid 31418. (Contributed by NM, 24-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( b  e.  T  /\  b  =/=  (  _I  |`  B ) ) ) )  ->  ( Z  .\/  ( R `
  b ) )  =  ( P  .\/  ( R `  b ) ) )
 
Theoremcdlemkfid2N 31405 Lemma for cdlemkfid3N 31407. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  =  N )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  b  e.  T )  /\  ( ( R `  b )  =/=  ( R `  F )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  Z  =  ( b `  P ) )
 
Theoremcdlemkid2 31406* Lemma for cdlemkid 31418. (Contributed by NM, 24-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  G  =  (  _I  |`  B )  /\  ( b  e.  T  /\  b  =/=  (  _I  |`  B ) ) ) )  ->  [_ G  /  g ]_ Y  =  P )
 
Theoremcdlemkfid3N 31407* TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  =  N ) 
 /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  G  e.  T  /\  ( b  e.  T  /\  b  =/=  (  _I  |`  B ) ) )  /\  (
 ( R `  b
 )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  [_ G  /  g ]_ Y  =  ( G `  P ) )
 
Theoremcdlemky 31408* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up  ( b Y G ) stuff.  V represents  Y in cdlemk31 31378. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  (
 ( P  .\/  ( R `  f ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( (
 ( S `  d
 ) `  P )  .\/  ( R `  (
 e  o.  `' d
 ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) ) )  ->  [_ G  /  g ]_ Y  =  ( ( b V G ) `  P ) )
 
Theoremcdlemkyu 31409* Convert between function and explicit forms.  C represents  Z in cdlemkuu 31377. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  (
 ( P  .\/  ( R `  f ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( (
 ( S `  d
 ) `  P )  .\/  ( R `  (
 e  o.  `' d
 ) ) ) ) ) )   &    |-  Q  =  ( S `  b )   &    |-  C  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  (
 ( P  .\/  ( R `  e ) ) 
 ./\  ( ( Q `
  P )  .\/  ( R `  ( e  o.  `' b ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) ) )  ->  [_ G  /  g ]_ Y  =  ( ( C `  G ) `  P ) )
 
Theoremcdlemkyuu 31410* cdlemkyu 31409 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  (
 ( P  .\/  ( R `  f ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  C  =  ( e  e.  T  |->  (
 iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  b ) `  P )  .\/  ( R `
  ( e  o.  `' b ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) ) ) ) 
 ->  [_ G  /  g ]_ Y  =  (
 ( C `  G ) `  P ) )
 
Theoremcdlemk11ta 31411* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  (
 ( P  .\/  ( R `  f ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  C  =  ( e  e.  T  |->  (
 iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  b ) `  P )  .\/  ( R `
  ( e  o.  `' b ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  I ) ) ) )  ->  [_ G  /  g ]_ Y  .<_  (
 [_ I  /  g ]_ Y  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk19ylem 31412* Lemma for cdlemk19y 31414. (Contributed by NM, 30-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  (
 ( P  .\/  ( R `  f ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  C  =  ( e  e.  T  |->  (
 iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  b ) `  P )  .\/  ( R `
  ( e  o.  `' b ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) ) )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F ) ) ) )  ->  [_ F  /  g ]_ Y  =  ( N `  P ) )
 
Theoremcdlemk11tb 31413* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. cdlemk11ta 31411 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) 
 /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  I ) ) ) )  ->  [_ G  /  g ]_ Y  .<_  (
 [_ I  /  g ]_ Y  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk19y 31414* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F ) ) ) ) 
 ->  [_ F  /  g ]_ Y  =  ( N `  P ) )
 
Theoremcdlemkid3N 31415* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  G  =  (  _I  |`  B )
 ) )  ->  [_ G  /  g ]_ X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  ( z `  P )  =  P )
 ) )
 
Theoremcdlemkid4 31416* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  G  =  (  _I  |`  B )
 ) )  ->  [_ G  /  g ]_ X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  z  =  (  _I  |`  B ) ) ) )
 
Theoremcdlemkid5 31417* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  G  =  (  _I  |`  B )
 ) )  ->  [_ G  /  g ]_ X  e.  T )
 
Theoremcdlemkid 31418* The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  G  =  (  _I  |`  B )
 ) )  ->  [_ G  /  g ]_ X  =  (  _I  |`  B )
 )
 
Theoremcdlemk35s 31419* Substitution version of cdlemk35 31394. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) )  /\  N  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) ) )  ->  [_ G  /  g ]_ X  e.  T )
 
Theoremcdlemk35s-id 31420* Substitution version of cdlemk35 31394. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  G  e.  T  /\  N  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) ) )  ->  [_ G  /  g ]_ X  e.  T )
 
Theoremcdlemk39s 31421* Substitution version of cdlemk39 31398. TODO: Can any commonality with cdlemk35s 31419 be exploited? (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) )  /\  N  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) ) )  ->  ( R `  [_ G  /  g ]_ X ) 
 .<_  ( R `  G ) )
 
Theoremcdlemk39s-id 31422* Substitution version of cdlemk39 31398 with non-identity requirement on  G removed. TODO: Can any commonality with cdlemk35s 31419 be exploited? (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  G  e.  T  /\  N  e.  T )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) ) )  ->  ( R `  [_ G  /  g ]_ X ) 
 .<_  ( R `  G ) )
 
Theoremcdlemk42 31423* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) ) )  ->  ( [_ G  /  g ]_ X `  P )  =  [_ G  /  g ]_ Y )
 
Theoremcdlemk19xlem 31424* Lemma for cdlemk19x 31425. (Contributed by NM, 30-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F ) ) ) ) 
 ->  ( [_ F  /  g ]_ X `  P )  =  ( N `  P ) )
 
Theoremcdlemk19x 31425* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 ->  ( [_ F  /  g ]_ X `  P )  =  ( N `  P ) )
 
Theoremcdlemk42yN 31426* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) ) )  ->  ( [_ G  /  g ]_ X `  P )  =  ( ( P 
 .\/  ( R `  G ) )  ./\  ( Z  .\/  ( R `
  ( G  o.  `' b ) ) ) ) )
 
Theoremcdlemk11tc 31427* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) 
 /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  I ) ) ) )  ->  ( [_ G  /  g ]_ X `  P ) 
 .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk11t 31428* Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  ( [_ G  /  g ]_ X `  P ) 
 .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk45 31429* Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119.  G,  I stand for g, h.  X represents tau. They do not explicitly mention the requirement  ( G  o.  I
)  =/=  (  _I  |  `  B ). (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( G  o.  I )  =/=  (  _I  |`  B ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) )
 
Theoremcdlemk46 31430* Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( G  o.  I )  =/=  (  _I  |`  B ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  .<_  ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) )
 
Theoremcdlemk47 31431* Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  =  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) 
 ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) ) )
 
Theoremcdlemk48 31432* Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  [_ G  /  g ]_ X ) ) )
 
Theoremcdlemk49 31433* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  [_ I  /  g ]_ X ) ) )
 
Theoremcdlemk50 31434* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. TODO: Combine into cdlemk52 31436? (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `
  [_ I  /  g ]_ X ) )  ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  [_ G  /  g ]_ X ) ) ) )
 
Theoremcdlemk51 31435* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. TODO: Combine into cdlemk52 31436? (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `
  [_ I  /  g ]_ X ) )  ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  [_ G  /  g ]_ X ) ) ) 
 .<_  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) 
 ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) ) )
 
Theoremcdlemk52 31436* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  ( ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  =  ( [_ ( G  o.  I )  /  g ]_ X `  P ) )
 
Theoremcdlemk53a 31437* Lemma for cdlemk53 31439. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk53b 31438* Lemma for cdlemk53 31439. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk53 31439* Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  ( R `  G )  =/=  ( R `  I
 ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk54 31440* Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( I  e.  T  /\  ( R `  G )  =  ( R `  I ) )  /\  j  e.  T  /\  ( j  =/=  (  _I  |`  B )  /\  ( R `  j )  =/=  ( R `  G )  /\  ( R `
  j )  =/=  ( R `  ( G  o.  I ) ) ) ) )  ->  ( [_ ( G  o.  I )  /  g ]_ X  o.  [_ j  /  g ]_ X )  =  ( ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X )  o.  [_ j  /  g ]_ X ) )
 
Theoremcdlemk55a 31441* Lemma for cdlemk55 31443. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( I  e.  T  /\  ( R `  G )  =  ( R `  I ) )  /\  j  e.  T  /\  ( j  =/=  (  _I  |`  B )  /\  ( R `  j )  =/=  ( R `  G )  /\  ( R `
  j )  =/=  ( R `  ( G  o.  I ) ) ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk55b 31442* Lemma for cdlemk55 31443. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  ( R `  G )  =  ( R `  I
 ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk55 31443* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
TheoremcdlemkyyN 31444* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up  ( b Y G ) stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `
  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( (
 ( S `  d
 ) `  P )  .\/  ( R `  (
 e  o.  `' d
 ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B ) 
 /\  N  e.  T )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  (
 b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) ) ) ) 
 ->  ( [_ G  /  g ]_ X `  P )  =  ( (
 b V G ) `
  P ) )
 
Theoremcdlemk43N 31445* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  N  e.  T  /\  F  =/=  N ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  (
 b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) ) ) ) 
 ->  ( ( U `  G ) `  P )  =  [_ G  /  g ]_ Y )
 
Theoremcdlemk35u 31446* Substitution version of cdlemk35 31394. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  N  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  G )  e.  T )
 
Theoremcdlemk55u1 31447* Lemma for cdlemk55u 31448. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  F )  =  ( R `  N )  /\  F  =/=  N )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  ( G  o.  I ) )  =  ( ( U `  G )  o.  ( U `  I ) ) )
 
Theoremcdlemk55u 31448* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  ( G  o.  I
 ) )  =  ( ( U `  G )  o.  ( U `  I ) ) )
 
Theoremcdlemk39u1 31449* Lemma for cdlemk39u 31450. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  N  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 ->  ( R `  ( U `  G ) ) 
 .<_  ( R `  G ) )
 
Theoremcdlemk39u 31450* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by  ( U `  G ). (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  ( U `  G ) )  .<_  ( R `
  G ) )
 
Theoremcdlemk19u1 31451* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  F  =/=  N  /\  N  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( U `  F ) `  P )  =  ( N `  P ) )
 
Theoremcdlemk19u 31452* Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with  F,  N,  U. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  N  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  F )  =  N )
 
Theoremcdlemk56 31453* Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e.  U is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 ->  U  e.  E )
 
Theoremcdlemk19w 31454* Use a fixed element to eliminate  P in cdlemk19u 31452. (Contributed by NM, 1-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  ._|_  =  ( oc `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  P  =  (  ._|_  `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N ) )  ->  ( U `  F )  =  N )
 
Theoremcdlemk56w 31455* Use a fixed element to eliminate  P in cdlemk56 31453. (Contributed by NM, 1-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  ._|_  =  ( oc `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  P  =  (  ._|_  `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N ) )  ->  ( U  e.  E  /\  ( U `  F )  =  N )
 )
 
Theoremcdlemk 31456* Lemma K of [Crawley] p.