HomeHome Metamath Proof Explorer
Theorem List (p. 312 of 322)
< 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-21498)
  Hilbert Space Explorer  Hilbert Space Explorer
(21499-23021)
  Users' Mathboxes  Users' Mathboxes
(23022-32154)
 

Theorem List for Metamath Proof Explorer - 31101-31200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemk35 31101* Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 31100 with shorter hypotheses. (Contributed by NM, 18-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 ) ) )  ->  X  e.  T )
 
Theoremcdlemk36 31102* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-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 ) ) ) )  ->  ( X `  P )  =  Y )
 
Theoremcdlemk37 31103* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-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 ) ) ) )  ->  ( X `  P )  .<_  ( P  .\/  ( R `  G ) ) )
 
Theoremcdlemk38 31104* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 2658? (Contributed by NM, 19-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 ) ) )  ->  ( X `  P ) 
 .<_  ( P  .\/  ( R `  G ) ) )
 
Theoremcdlemk39 31105* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of tau, represented by  X. (Contributed by NM, 19-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 `  X ) 
 .<_  ( R `  G ) )
 
Theoremcdlemk40 31106* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)
 |-  X  =  ( iota_ z  e.  T ph )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X ) )   =>    |-  ( G  e.  T  ->  ( U `  G )  =  if ( F  =  N ,  G ,  [_ G  /  g ]_ X ) )
 
Theoremcdlemk40t 31107* 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 )
 
Theoremcdlemk40f 31108* 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 31109* 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 31110 Lemma for cdlemkfid3N 31114. (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 31111 Lemma for cdlemkid 31125. (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 31112 Lemma for cdlemkfid3N 31114. (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 31113* Lemma for cdlemkid 31125. (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 31114* 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 31115* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up  ( b Y G ) stuff.  V represents  Y in cdlemk31 31085. (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 31116* Convert between function and explicit forms.  C represents  Z in cdlemkuu 31084. 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 31117* cdlemkyu 31116 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 31118* 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 31119* Lemma for cdlemk19y 31121. (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 31120* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. cdlemk11ta 31118 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 31121* cdlemk19 31058 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 31122* Lemma for cdlemkid 31125. (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 31123* Lemma for cdlemkid 31125. (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 31124* Lemma for cdlemkid 31125. (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 31125* 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 31126* Substitution version of cdlemk35 31101. (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 31127* Substitution version of cdlemk35 31101. (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 31128* Substitution version of cdlemk39 31105. TODO: Can any commonality with cdlemk35s 31126 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 31129* Substitution version of cdlemk39 31105 with non-identity requirement on  G removed. TODO: Can any commonality with cdlemk35s 31126 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 31130* 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 31131* Lemma for cdlemk19x 31132. (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 31132* cdlemk19 31058 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 31133* 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 31134* 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 31135* 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 31136* 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 31137* 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 31138* 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 31139* 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 31140* 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 31141* 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 31143? (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 31142* 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 31143? (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 31143* 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 31144* Lemma for cdlemk53 31146. (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 31145* Lemma for cdlemk53 31146. (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 31146* 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 31147* 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 31148* Lemma for cdlemk55 31150. (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 31149* Lemma for cdlemk55 31150. (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 31150* 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 31151* 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 31152* 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 31153* Substitution version of cdlemk35 31101. (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 31154* Lemma for cdlemk55u 31155. (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 31155* 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 31156* Lemma for cdlemk39u 31157. (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 )