HomeHome Metamath Proof Explorer
Theorem List (p. 303 of 313)
< 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-21423)
  Hilbert Space Explorer  Hilbert Space Explorer
(21424-22946)
  Users' Mathboxes  Users' Mathboxes
(22947-31284)
 

Theorem List for Metamath Proof Explorer - 30201-30300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemkj-2N 30201* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  Y  =  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( G  o.  `' C ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  C )  =/=  ( R `  F )  /\  ( R `  C )  =/=  ( R `  G ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  Y  e.  T )
 
Theoremcdlemkuv-2N 30202* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma2 (p) function, given  V. (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( G  e.  T  ->  ( V `  G )  =  ( iota_ k  e.  T ( k `  P )  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( Q `
  P )  .\/  ( R `  ( G  o.  `' C ) ) ) ) ) )
 
Theoremcdlemkuel-2N 30203* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 30182? (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  C )  =/=  ( R `  F )  /\  ( R `  C )  =/=  ( R `  G ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( V `  G )  e.  T )
 
Theoremcdlemkuv2-2 30204* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 2, where sigma2 (p) is  V, f2 is  C, and k2 is  Q. (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  C )  =/=  ( R `  F )  /\  ( R `  C )  =/=  ( R `  G ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( V `  G ) `  P )  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( Q `
  P )  .\/  ( R `  ( G  o.  `' C ) ) ) ) )
 
Theoremcdlemk18-2N 30205* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119.  N,  V,  Q,  C are k, sigma2 (p), k2, f2. (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( ( R `  C )  =/=  ( R `  F )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  C  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( N `  P )  =  ( ( V `
  F ) `  P ) )
 
Theoremcdlemk19-2N 30206* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119.  N,  V,  Q,  C are k, sigma2 (p), k2, f2. (Contributed by NM, 2-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( ( R `  C )  =/=  ( R `  F )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  C  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( V `  F )  =  N )
 
Theoremcdlemk7u-2N 30207* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma2 case. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   &    |-  Z  =  ( ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  ( ( R `
  ( G  o.  `' C ) )  .\/  ( R `  ( X  o.  `' C ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  C  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( X  e.  T  /\  X  =/=  (  _I  |`  B ) ) )  /\  ( ( ( R `  C )  =/=  ( R `  F )  /\  ( R `
  G )  =/=  ( R `  C )  /\  ( R `  X )  =/=  ( R `  C ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  (
 ( V `  G ) `  P )  .<_  ( ( ( V `  X ) `  P )  .\/  Z ) )
 
Theoremcdlemk11u-2N 30208* Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma2 ( Z) case. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   &    |-  Z  =  ( ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  ( ( R `
  ( G  o.  `' C ) )  .\/  ( R `  ( X  o.  `' C ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  C  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( X  e.  T  /\  X  =/=  (  _I  |`  B ) ) )  /\  ( ( ( R `  C )  =/=  ( R `  F )  /\  ( R `
  G )  =/=  ( R `  C )  /\  ( R `  X )  =/=  ( R `  C ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  (
 ( V `  G ) `  P )  .<_  ( ( ( V `  X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
 
Theoremcdlemk12u-2N 30209* Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma2 ( V) case. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  e.  T  /\  X  =/=  (  _I  |`  B ) ) ) 
 /\  ( ( ( R `  C )  =/=  ( R `  F )  /\  ( R `
  G )  =/=  ( R `  C )  /\  ( R `  X )  =/=  ( R `  C ) ) 
 /\  ( ( R `
  G )  =/=  ( R `  X )  /\  F  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( V `  G ) `  P )  =  (
 ( P  .\/  ( G `  P ) ) 
 ./\  ( ( ( V `  X ) `
  P )  .\/  ( R `  ( X  o.  `' G ) ) ) ) )
 
Theoremcdlemk21-2N 30210* Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=2. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( ( ( R `  C )  =/=  ( R `  F )  /\  ( R `
  G )  =/=  ( R `  C ) )  /\  ( ( R `  G )  =/=  ( R `  F )  /\  F  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  (
 ( S `  G ) `  P )  =  ( ( V `  G ) `  P ) )
 
Theoremcdlemk20-2N 30211* Part of proof of Lemma K of [Crawley] p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be fi. Our  D,  C,  O,  Q,  U,  V represent their f1, f2, k1, k2, sigma1, sigma2. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  C  e.  T  /\  N  e.  T )  /\  ( D  e.  T  /\  D  =/=  (  _I  |`  B ) )  /\  ( C  e.  T  /\  C  =/=  (  _I  |`  B ) ) ) 
 /\  ( ( ( R `  C )  =/=  ( R `  F )  /\  ( R `
  D )  =/=  ( R `  F )  /\  ( R `  D )  =/=  ( R `  C ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  (
 ( V `  D ) `  P )  =  ( O `  P ) )
 
Theoremcdlemk22 30212* Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 5-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   &    |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T ( k `
  P )  =  ( ( P  .\/  ( R `  d ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  (
 ( P  .\/  ( R `  e ) ) 
 ./\  ( ( O `
  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( ( N  e.  T  /\  G  e.  T  /\  C  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( C  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  C )  /\  ( R `
  C )  =/=  ( R `  F ) )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( R `
  G )  =/=  ( R `  D )  /\  ( R `  C )  =/=  ( R `  D ) ) ) )  ->  (
 ( U `  G ) `  P )  =  ( ( V `  G ) `  P ) )
 
Theoremcdlemk30 30213* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  e.  T  /\  b  e.  T  /\  N  e.  T ) 
 /\  ( ( R `
  b )  =/=  ( R `  F )  /\  ( F  =/=  (  _I  |`  B )  /\  b  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( S `  b ) `  P )  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) ) )
 
Theoremcdlemkuu 30214* Convert between function and operation forms of  Y. TODO: Use operation form everywhere. (Contributed by NM, 6-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  d ) `  P )  .\/  ( R `
  ( e  o.  `' d ) ) ) ) ) )   &    |-  Q  =  ( S `  D )   &    |-  Z  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   =>    |-  ( ( D  e.  T  /\  G  e.  T )  ->  ( D Y G )  =  ( Z `  G ) )
 
Theoremcdlemk31 30215* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  b  e.  T  /\  N  e.  T )  /\  G  e.  T )  /\  ( ( ( R `  b
 )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  b  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( (
 b Y G ) `
  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( (
 ( S `  b
 ) `  P )  .\/  ( R `  ( G  o.  `' b ) ) ) ) )
 
Theoremcdlemk32 30216* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  b  e.  T  /\  N  e.  T )  /\  G  e.  T )  /\  ( ( ( R `  b
 )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  b  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( (
 b Y G ) `
  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( (
 ( P  .\/  ( R `  b ) ) 
 ./\  ( ( N `
  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )  .\/  ( R `  ( G  o.  `' b ) ) ) ) )
 
Theoremcdlemkuel-3 30217* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 30182? (Contributed by NM, 11-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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 )  /\  G  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  D )  =/=  ( R `  G ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( D Y G )  e.  T )
 
Theoremcdlemkuv2-3N 30218* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma2 (p) is  Y, f1 is  D, and k1 is  O. (Contributed by NM, 6-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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 )  /\  G  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  D )  =/=  ( R `  G ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( D Y G ) `  P )  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( ( S `  D ) `
  P )  .\/  ( R `  ( G  o.  `' D ) ) ) ) )
 
Theoremcdlemk18-3N 30219* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119.  N,  Y,  O,  D are k, sigma2 (p), k1, f1. (Contributed by NM, 7-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( D Y F ) `  P )  =  ( N `  P ) )
 
Theoremcdlemk22-3 30220* Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 7-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T ) 
 /\  ( ( N  e.  T  /\  G  e.  T  /\  C  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( C  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  C )  /\  ( R `  C )  =/=  ( R `  F ) )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `
  C )  =/=  ( R `  D ) ) ) ) 
 ->  ( ( D Y G ) `  P )  =  ( ( C Y G ) `  P ) )
 
Theoremcdlemk23-3 30221* Part of proof of Lemma K of [Crawley] p. 118. Eliminate the  ( R `  C )  =/=  ( R `  D ) requirement from cdlemk22-3 30220. (Contributed by NM, 7-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  C  e.  T  /\  x  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  (  _I  |`  B ) 
 /\  D  =/=  (  _I  |`  B ) ) 
 /\  ( G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B )  /\  x  =/=  (  _I  |`  B ) ) )  /\  (
 ( ( R `  G )  =/=  ( R `  C )  /\  ( R `  C )  =/=  ( R `  F )  /\  ( R `
  D )  =/=  ( R `  F ) )  /\  ( ( R `  G )  =/=  ( R `  D )  /\  ( R `
  x )  =/=  ( R `  C ) )  /\  ( ( R `  x )  =/=  ( R `  D )  /\  ( R `
  x )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  x ) ) ) )  ->  (
 ( D Y G ) `  P )  =  ( ( C Y G ) `  P ) )
 
Theoremcdlemk24-3 30222* Part of proof of Lemma K of [Crawley] p. 118. Eliminate the  ( R `  x )  =/=  ( R `  C ) requirement from cdlemk23-3 30221 using  ( R `  C )  =  ( R `  D ). (Contributed by NM, 7-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  C  e.  T  /\  x  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  (  _I  |`  B ) 
 /\  D  =/=  (  _I  |`  B ) ) 
 /\  ( G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B )  /\  x  =/=  (  _I  |`  B ) ) )  /\  (
 ( ( R `  G )  =/=  ( R `  C )  /\  ( R `  C )  =/=  ( R `  F )  /\  ( R `
  D )  =/=  ( R `  F ) )  /\  ( ( R `  G )  =/=  ( R `  D )  /\  ( R `
  C )  =  ( R `  D ) )  /\  ( ( R `  x )  =/=  ( R `  D )  /\  ( R `
  x )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  x ) ) ) )  ->  (
 ( D Y G ) `  P )  =  ( ( C Y G ) `  P ) )
 
Theoremcdlemk25-3 30223* Part of proof of Lemma K of [Crawley] p. 118. Eliminate the  ( R `  C )  =  ( R `  D ) requirement from cdlemk24-3 30222. (Contributed by NM, 7-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  C  e.  T  /\  x  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  (  _I  |`  B ) 
 /\  D  =/=  (  _I  |`  B ) ) 
 /\  ( G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B )  /\  x  =/=  (  _I  |`  B ) ) )  /\  (
 ( ( R `  G )  =/=  ( R `  C )  /\  ( R `  C )  =/=  ( R `  F )  /\  ( R `
  D )  =/=  ( R `  F ) )  /\  ( R `
  G )  =/=  ( R `  D )  /\  ( ( R `
  x )  =/=  ( R `  D )  /\  ( R `  x )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  x ) ) ) )  ->  ( ( D Y G ) `  P )  =  (
 ( C Y G ) `  P ) )
 
Theoremcdlemk26b-3 30224* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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 )  /\  N  e.  T )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B )  /\  ( R `  F )  =  ( R `  N ) ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  E. x  e.  T  ( ( x  =/=  (  _I  |`  B ) 
 /\  ( R `  x )  =/=  ( R `  F )  /\  ( R `  x )  =/=  ( R `  G ) )  /\  ( x Y G )  e.  T ) )
 
Theoremcdlemk26-3 30225* Part of proof of Lemma K of [Crawley] p. 118. Eliminate the  x requirements from cdlemk25-3 30223. (Contributed by NM, 10-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  C  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  (  _I  |`  B ) 
 /\  D  =/=  (  _I  |`  B ) ) 
 /\  ( G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) ) ) 
 /\  ( ( ( R `  G )  =/=  ( R `  C )  /\  ( R `
  C )  =/=  ( R `  F )  /\  ( R `  D )  =/=  ( R `  F ) ) 
 /\  ( R `  G )  =/=  ( R `  D ) ) )  ->  ( ( D Y G ) `  P )  =  (
 ( C Y G ) `  P ) )
 
Theoremcdlemk27-3 30226* Part of proof of Lemma K of [Crawley] p. 118. Eliminate the  P from the conclusion of cdlemk25-3 30223. (Contributed by NM, 10-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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  /\  D  e.  T  /\  N  e.  T ) 
 /\  ( G  e.  T  /\  C  e.  T ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  (  _I  |`  B ) 
 /\  D  =/=  (  _I  |`  B ) ) 
 /\  ( G  =/=  (  _I  |`  B )  /\  C  =/=  (  _I  |`  B ) ) ) 
 /\  ( ( ( R `  G )  =/=  ( R `  C )  /\  ( R `
  C )  =/=  ( R `  F )  /\  ( R `  D )  =/=  ( R `  F ) ) 
 /\  ( R `  G )  =/=  ( R `  D ) ) )  ->  ( D Y G )  =  ( C Y G ) )
 
Theoremcdlemk28-3 30227* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( 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 ) ) ) 
 ->  E. z  e.  T  A. b  e.  T  ( ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) )  ->  z  =  ( b Y G ) ) )
 
Theoremcdlemk33N 30228* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. TODO: not needed, is embodied in cdlemk34 30229. (Contributed by NM, 18-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  d ) `  P )  .\/  ( R `
  ( e  o.  `' d ) ) ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  z  =  ( b Y G ) ) )   =>    |-  ( ( ( 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 ) ) )  ->  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  ( z `  P )  =  ( (
 b Y G ) `
  P ) ) ) )
 
Theoremcdlemk34 30229* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify 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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  d ) `  P )  .\/  ( R `
  ( e  o.  `' d ) ) ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  z  =  ( b Y G ) ) )   =>    |-  ( ( ( 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  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  ( z `  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( ( ( P 
 .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) )  .\/  ( R `  ( G  o.  `' b ) ) ) ) ) ) )
 
Theoremcdlemk29-3 30230* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-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 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  Y  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( ( S `
  d ) `  P )  .\/  ( R `
  ( e  o.  `' d ) ) ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) )  ->  z  =  ( b Y G ) ) )   =>    |-  ( ( ( 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 )
 
Theoremcdlemk35 30231* Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 30230 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 30232* 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 30233* 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 30234* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 2629? (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 30235* 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 30236* 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 30237* 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 30238* 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 30239* 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 30240 Lemma for cdlemkfid3N 30244. (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 30241 Lemma for cdlemkid 30255. (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 30242 Lemma for cdlemkfid3N 30244. (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 30243* Lemma for cdlemkid 30255. (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 30244* 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 30245* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up  ( b Y G ) stuff.  V represents  Y in cdlemk31 30215. (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 30246* Convert between function and explicit forms.  C represents  Z in cdlemkuu 30214. 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 30247* cdlemkyu 30246 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 30248* 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 30249* Lemma for cdlemk19y 30251. (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 30250* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. cdlemk11ta 30248 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 30251* cdlemk19 30188 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 30252* Lemma for cdlemkid 30255. (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 30253* Lemma for cdlemkid 30255. (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 30254* Lemma for cdlemkid 30255. (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 )  =  (