HomeHome Metamath Proof Explorer
Theorem List (p. 364 of 377)
< 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-25811)
  Hilbert Space Explorer  Hilbert Space Explorer
(25812-27336)
  Users' Mathboxes  Users' Mathboxes
(27337-37662)
 

Theorem List for Metamath Proof Explorer - 36301-36400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemk5a 36301 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-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 )  /\  ( F  e.  T  /\  G  e.  T  /\  X  e.  T ) 
 /\  ( ( R `
  G )  =/=  ( R `  F )  /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  (
 ( ( F `  P )  .\/  ( R `
  F ) ) 
 ./\  ( ( F `
  P )  .\/  ( R `  ( G  o.  `' F ) ) ) )  .<_  ( ( X `  P )  .\/  ( R `  ( X  o.  `' F ) ) ) )
 
Theoremcdlemk5 36302 Part of proof of Lemma K of [Crawley] p. 118. (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 )   =>    |-  (
 ( ( ( 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 )  /\  ( R `  G )  =/=  ( R `  F ) ) )  ->  ( ( P  .\/  ( N `  P ) )  ./\  ( ( G `  P )  .\/  ( R `  ( G  o.  `' F ) ) ) )  .<_  ( ( X `  P )  .\/  ( R `  ( X  o.  `' F ) ) ) )
 
Theoremcdlemk6 36303 Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35350. (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 )   =>    |-  (
 ( ( ( 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 )  /\  (
 ( R `  G )  =/=  ( R `  F )  /\  ( R `
  X )  =/=  ( R `  F ) ) ) ) 
 ->  ( ( P  .\/  ( G `  P ) )  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F ) ) ) )  .<_  ( ( ( ( G `
  P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )  .\/  ( ( ( X `
  P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) ) )
 
Theoremcdlemk8 36304 Part of proof of Lemma K of [Crawley] p. 118. (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 )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( G  e.  T  /\  X  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  (
 ( G `  P )  .\/  ( X `  P ) )  =  ( ( G `  P )  .\/  ( R `
  ( X  o.  `' G ) ) ) )
 
Theoremcdlemk9 36305 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 36306 Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 36305 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 36307* Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 36311. (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 36308 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 36309 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 36310* 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 36311* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 36307? (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 36312* 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 36313* 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 36314* 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 36315* 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 36316* 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 36317* 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 36318* 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 36319* 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 36320* 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 36321* 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 36322* 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 36323* 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 36324* 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 36325* 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 36326* 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 36327* 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 36328* Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35350. (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 36329* 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 36330* 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 36331* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 36329? (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 36332* 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 36333* 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 36334* 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 36335* 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 36336* 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 36337* 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 36338* 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 36339* 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 36340* 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 36341* 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 36342* 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 36343* 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 36344* 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 36345* 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 36346* 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 36347* 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 36348* 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 36349* 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 36350* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 36329? (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 36351* 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 36352* 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 36353* 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 36354* 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 36355* 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 36356* 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 36357* 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 36358* 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 36359* 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 )  /\