HomeHome Metamath Proof Explorer
Theorem List (p. 305 of 316)
< 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-31527)
 

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemk9 30401 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  W )  =  ( R `  ( X  o.  `' G ) ) )
 
Theoremcdlemk9bN 30402 Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 30401 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  W )  =  ( R `  ( G  o.  `' X ) ) )
 
Theoremcdlemki 30403* Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 30407. (Contributed by NM, 25-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  I  =  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( G  o.  `' F ) ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  F ) ) )  ->  I  e.  T )
 
Theoremcdlemkvcl 30404 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  V  =  ( ( ( G `
  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  P  e.  A ) 
 ->  V  e.  B )
 
Theoremcdlemk10 30405 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  V  =  ( ( ( G `
  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  V  .<_  ( R `  ( X  o.  `' G ) ) )
 
Theoremcdlemksv 30406* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   =>    |-  ( G  e.  T  ->  ( S `  G )  =  ( iota_
 i  e.  T ( i `  P )  =  ( ( P 
 .\/  ( R `  G ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( G  o.  `' F ) ) ) ) ) )
 
Theoremcdlemksel 30407* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 30403? (Contributed by NM, 26-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  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 ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  F ) ) ) 
 ->  ( S `  G )  e.  T )
 
Theoremcdlemksat 30408* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  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 ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  F ) ) ) 
 ->  ( ( S `  G ) `  P )  e.  A )
 
Theoremcdlemksv2 30409* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function  S at the fixed  P parameter. (Contributed by NM, 26-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  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 ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  F ) ) ) 
 ->  ( ( S `  G ) `  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( G  o.  `' F ) ) ) ) )
 
Theoremcdlemk7 30410* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( ( ( G `
  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( ( N  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
  G )  =/=  ( R `  F )  /\  ( R `  X )  =/=  ( R `  F ) ) )  ->  ( ( S `  G ) `  P )  .<_  ( ( ( S `  X ) `  P )  .\/  V ) )
 
Theoremcdlemk11 30411* Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( ( ( G `
  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( ( N  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
  G )  =/=  ( R `  F )  /\  ( R `  X )  =/=  ( R `  F ) ) )  ->  ( ( S `  G ) `  P )  .<_  ( ( ( S `  X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
 
Theoremcdlemk12 30412* Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  ./\  =  ( meet `  K )   &    |-  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 ) 
 /\  F  e.  T  /\  G  e.  T ) 
 /\  ( ( N  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( ( R `  G )  =/=  ( R `  F )  /\  ( R `
  X )  =/=  ( R `  F ) )  /\  ( R `
  G )  =/=  ( R `  X ) ) )  ->  ( ( S `  G ) `  P )  =  ( ( P  .\/  ( G `  P ) )  ./\  ( ( ( S `
  X ) `  P )  .\/  ( R `
  ( X  o.  `' G ) ) ) ) )
 
Theoremcdlemkoatnle 30413* Utility lemma. (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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( ( O `  P )  e.  A  /\  -.  ( O `  P )  .<_  W ) )
 
Theoremcdlemk13 30414* Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119.  O,  D are k1, f1. (Contributed by NM, 1-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( O `  P )  =  ( ( P 
 .\/  ( R `  D ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( D  o.  `' F ) ) ) ) )
 
Theoremcdlemkole 30415* Utility lemma. (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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( O `  P ) 
 .<_  ( P  .\/  ( R `  D ) ) )
 
Theoremcdlemk14 30416* Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119.  O,  D are k1, f1. (Contributed by NM, 1-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( N `  P ) 
 .<_  ( ( O `  P )  .\/  ( R `
  ( F  o.  `' D ) ) ) )
 
Theoremcdlemk15 30417* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119.  O,  D are k1, f1. (Contributed by NM, 1-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( N `  P ) 
 .<_  ( ( P  .\/  ( R `  F ) )  ./\  ( ( O `  P )  .\/  ( R `  ( F  o.  `' D ) ) ) ) )
 
Theoremcdlemk16a 30418* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-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 ) ) ) ) ) )   &    |-  O  =  ( S `  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 ) ) )  ->  ( (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( O `
  P )  .\/  ( R `  ( G  o.  `' D ) ) ) )  e.  A  /\  -.  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( O `
  P )  .\/  ( R `  ( G  o.  `' D ) ) ) )  .<_  W ) )
 
Theoremcdlemk16 30419* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( ( ( P 
 .\/  ( R `  F ) )  ./\  ( ( O `  P )  .\/  ( R `
  ( F  o.  `' D ) ) ) )  e.  A  /\  -.  ( ( P  .\/  ( R `  F ) )  ./\  ( ( O `  P )  .\/  ( R `  ( F  o.  `' D ) ) ) )  .<_  W ) )
 
Theoremcdlemk17 30420* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119.  O,  D are k1, f1. (Contributed by NM, 1-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( N `  P )  =  ( ( P 
 .\/  ( R `  F ) )  ./\  ( ( O `  P )  .\/  ( R `
  ( F  o.  `' D ) ) ) ) )
 
Theoremcdlemk1u 30421* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( P  .\/  ( O `
  P ) ) 
 .<_  ( ( D `  P )  .\/  ( R `
  D ) ) )
 
Theoremcdlemk5auN 30422* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( D  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  ( ( R `  G )  =/=  ( R `  D )  /\  ( D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( (
 ( D `  P )  .\/  ( R `  D ) )  ./\  ( ( D `  P )  .\/  ( R `
  ( G  o.  `' D ) ) ) )  .<_  ( ( X `
  P )  .\/  ( R `  ( X  o.  `' D ) ) ) )
 
Theoremcdlemk5u 30423* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( ( N  e.  T  /\  G  e.  T  /\  X  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X )  =/=  ( R `  D ) ) ) )  ->  ( ( P  .\/  ( O `  P ) )  ./\  ( ( G `  P )  .\/  ( R `
  ( G  o.  `' D ) ) ) )  .<_  ( ( X `
  P )  .\/  ( R `  ( X  o.  `' D ) ) ) )
 
Theoremcdlemk6u 30424* Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 29448. (Contributed by NM, 4-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( ( N  e.  T  /\  G  e.  T  /\  X  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X )  =/=  ( R `  D ) ) ) )  ->  ( ( P  .\/  ( G `  P ) )  ./\  ( ( O `  P )  .\/  ( R `
  ( G  o.  `' D ) ) ) )  .<_  ( ( ( ( G `  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' D ) )  .\/  ( R `
  ( X  o.  `' D ) ) ) )  .\/  ( (
 ( X `  P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' D ) )  .\/  ( O `
  P ) ) ) ) )
 
Theoremcdlemkj 30425* Part of proof of Lemma K of [Crawley] p. 118. (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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  Z  =  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  G ) )  ./\  ( ( O `  P )  .\/  ( R `  ( G  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 ) ) )  ->  Z  e.  T )
 
TheoremcdlemkuvN 30426* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma1 (p) function  U. (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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( O `  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   =>    |-  ( G  e.  T  ->  ( U `  G )  =  ( iota_ j  e.  T ( j `  P )  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( O `
  P )  .\/  ( R `  ( G  o.  `' D ) ) ) ) ) )
 
Theoremcdlemkuel 30427* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 30425? (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 ) ) ) ) ) )   &    |-  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 )  /\  ( 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 ) ) )  ->  ( U `  G )  e.  T )
 
Theoremcdlemkuat 30428* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-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 ) ) ) ) ) )   &    |-  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 )  /\  ( 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 ) ) )  ->  ( ( U `  G ) `  P )  e.  A )
 
Theoremcdlemkuv2 30429* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma1 (p) is  U, f1 is  D, and k1 is  O. (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 ) ) ) ) ) )   &    |-  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 )  /\  ( 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 ) ) )  ->  ( ( U `  G ) `  P )  =  (
 ( P  .\/  ( R `  G ) ) 
 ./\  ( ( O `
  P )  .\/  ( R `  ( G  o.  `' D ) ) ) ) )
 
Theoremcdlemk18 30430* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119.  N,  U,  O,  D are k, sigma1 (p), k1, f1. (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 ) ) ) ) ) )   &    |-  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  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( N `  P )  =  ( ( U `
  F ) `  P ) )
 
Theoremcdlemk19 30431* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119.  N,  U,  O,  D are k, sigma1 (p), k1, f1. (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 ) ) ) ) ) )   &    |-  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  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( U `  F )  =  N )
 
Theoremcdlemk7u 30432* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( O `  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   &    |-  V  =  ( ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  ( ( R `
  ( G  o.  `' D ) )  .\/  ( R `  ( X  o.  `' D ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  e.  T  /\  D  e.  T ) 
 /\  ( ( N  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  X  =/=  (  _I  |`  B )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `
  X )  =/=  ( R `  D ) ) ) ) 
 ->  ( ( U `  G ) `  P )  .<_  ( ( ( U `  X ) `
  P )  .\/  V ) )
 
Theoremcdlemk11u 30433* Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma1 ( U) case. (Contributed by NM, 4-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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( O `  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   &    |-  V  =  ( ( ( G `  P )  .\/  ( X `
  P ) ) 
 ./\  ( ( R `
  ( G  o.  `' D ) )  .\/  ( R `  ( X  o.  `' D ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  F  e.  T  /\  D  e.  T ) 
 /\  ( ( N  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  X  =/=  (  _I  |`  B )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `
  X )  =/=  ( R `  D ) ) ) ) 
 ->  ( ( U `  G ) `  P )  .<_  ( ( ( U `  X ) `
  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
 
Theoremcdlemk12u 30434* Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma1 ( U) case. (Contributed by NM, 4-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 ) ) ) ) ) )   &    |-  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  /\  X  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X ) )  /\  ( ( R `  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `
  X )  =/=  ( R `  D ) ) ) ) 
 ->  ( ( U `  G ) `  P )  =  ( ( P  .\/  ( G `  P ) )  ./\  ( ( ( U `
  X ) `  P )  .\/  ( R `
  ( X  o.  `' G ) ) ) ) )
 
Theoremcdlemk21N 30435* Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (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 ) ) ) ) ) )   &    |-  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 )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  G )  =/=  ( R `  F ) ) ) )  ->  ( ( S `  G ) `  P )  =  (
 ( U `  G ) `  P ) )
 
Theoremcdlemk20 30436* 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.)
 |-  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 ) ) ) ) ) )   &    |-  O  =  ( S `  D )   &    |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( ( O `  P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )   &    |-  Q  =  ( S `  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( ( N  e.  T  /\  C  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) 
 /\  C  =/=  (  _I  |`  B ) ) 
 /\  ( ( R `
  D )  =/=  ( R `  F )  /\  ( R `  C )  =/=  ( R `  F )  /\  ( R `  C )  =/=  ( R `  D ) ) ) )  ->  ( ( U `  C ) `  P )  =  ( Q `  P ) )
 
Theoremcdlemkoatnle-2N 30437* Utility lemma. (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 )   =>    |-  ( ( ( 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 ) ) )  ->  ( ( Q `  P )  e.  A  /\  -.  ( Q `  P )  .<_  W ) )
 
Theoremcdlemk13-2N 30438* Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119.  Q,  C are k2, f2. (Contributed by NM, 1-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 )   =>    |-  ( ( ( 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 ) ) )  ->  ( Q `  P )  =  ( ( P 
 .\/  ( R `  C ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( C  o.  `' F ) ) ) ) )
 
Theoremcdlemkole-2N 30439* Utility lemma. (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 )   =>    |-  ( ( ( 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 ) ) )  ->  ( Q `  P ) 
 .<_  ( P  .\/  ( R `  C ) ) )
 
Theoremcdlemk14-2N 30440* Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119.  Q,  C are k2, f2. (Contributed by NM, 1-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 )   =>    |-  ( ( ( 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 ) 
 .<_  ( ( Q `  P )  .\/  ( R `
  ( F  o.  `' C ) ) ) )
 
Theoremcdlemk15-2N 30441* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119.  Q,  C are k2, f2. (Contributed by NM, 1-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 )   =>    |-  ( ( ( 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 ) 
 .<_  ( ( P  .\/  ( R `  F ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( F  o.  `' C ) ) ) ) )
 
Theoremcdlemk16-2N 30442* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-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 )   =>    |-  ( ( ( 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 ) ) )  ->  ( ( ( P 
 .\/  ( R `  F ) )  ./\  ( ( Q `  P )  .\/  ( R `
  ( F  o.  `' C ) ) ) )  e.  A  /\  -.  ( ( P  .\/  ( R `  F ) )  ./\  ( ( Q `  P )  .\/  ( R `  ( F  o.  `' C ) ) ) )  .<_  W ) )
 
Theoremcdlemk17-2N 30443* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119.  Q,  C are k2, f2. (Contributed by NM, 1-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 )   =>    |-  ( ( ( 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 )  =  ( ( P 
 .\/  ( R `  F ) )  ./\  ( ( Q `  P )  .\/  ( R `
  ( F  o.  `' C ) ) ) ) )
 
Theoremcdlemkj-2N 30444* 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 30445* 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 30446* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 30425? (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 30447* 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 30448* 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 30449* 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 30450* 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 30451* 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 30452* 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 30453* 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 30454* 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 30455* 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 30456* 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 30457* 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 30458* 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 ) )