Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hspmbllem2 Structured version   Visualization version   Unicode version

Theorem hspmbllem2 38567
Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hspmbllem2.h  |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ k  e.  x  if ( k  =  l ,  ( -oo (,) y ) ,  RR ) ) )
hspmbllem2.x  |-  ( ph  ->  X  e.  Fin )
hspmbllem2.k  |-  ( ph  ->  K  e.  X )
hspmbllem2.y  |-  ( ph  ->  Y  e.  RR )
hspmbllem2.e  |-  ( ph  ->  E  e.  RR+ )
hspmbllem2.c  |-  ( ph  ->  C : NN --> ( RR 
^m  X ) )
hspmbllem2.d  |-  ( ph  ->  D : NN --> ( RR 
^m  X ) )
hspmbllem2.a  |-  ( ph  ->  A  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
hspmbllem2.g  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) ) ) )  <_  ( (
(voln* `  X ) `  A
)  +  E ) )
hspmbllem2.r  |-  ( ph  ->  ( (voln* `  X ) `  A
)  e.  RR )
hspmbllem2.i  |-  ( ph  ->  ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  e.  RR )
hspmbllem2.f  |-  ( ph  ->  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) )  e.  RR )
hspmbllem2.l  |-  L  =  ( x  e.  Fin  |->  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
hspmbllem2.t  |-  T  =  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) ) )
hspmbllem2.s  |-  S  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  =  K ,  if ( x  <_  ( c `  h ) ,  ( c `  h ) ,  x ) ,  ( c `  h
) ) ) ) )
Assertion
Ref Expression
hspmbllem2  |-  ( ph  ->  ( ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  +  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) ) )  <_  ( (
(voln* `  X ) `  A
)  +  E ) )
Distinct variable groups:    A, j,
k    C, a, b, c, h, k, l    D, a, b, c, h, j, k, l    j, H, k    K, a, b, c, h, j, k, l, x, y    S, a, b, k, l    T, a, b, k, l    X, a, b, c, h, j, k, l, x, y    Y, a, b, c, h, j, k, l, x, y    ph, a, b, c, h, j, k, l, x, y
Allowed substitution hints:    A( x, y, h, a, b, c, l)    C( x, y, j)    D( x, y)    S( x, y, h, j, c)    T( x, y, h, j, c)    E( x, y, h, j, k, a, b, c, l)    H( x, y, h, a, b, c, l)    L( x, y, h, j, k, a, b, c, l)

Proof of Theorem hspmbllem2
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 hspmbllem2.i . . 3  |-  ( ph  ->  ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  e.  RR )
2 hspmbllem2.f . . 3  |-  ( ph  ->  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) )  e.  RR )
31, 2readdcld 9688 . 2  |-  ( ph  ->  ( ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  +  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) ) )  e.  RR )
4 hspmbllem2.r . . . 4  |-  ( ph  ->  ( (voln* `  X ) `  A
)  e.  RR )
5 hspmbllem2.e . . . . 5  |-  ( ph  ->  E  e.  RR+ )
65rpred 11364 . . . 4  |-  ( ph  ->  E  e.  RR )
74, 6readdcld 9688 . . 3  |-  ( ph  ->  ( ( (voln* `  X ) `  A
)  +  E )  e.  RR )
8 nfv 1769 . . . 4  |-  F/ j
ph
9 nnex 10637 . . . . 5  |-  NN  e.  _V
109a1i 11 . . . 4  |-  ( ph  ->  NN  e.  _V )
11 icossicc 11746 . . . . 5  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
12 hspmbllem2.l . . . . . 6  |-  L  =  ( x  e.  Fin  |->  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
13 hspmbllem2.x . . . . . . 7  |-  ( ph  ->  X  e.  Fin )
1413adantr 472 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  X  e. 
Fin )
15 hspmbllem2.c . . . . . . . 8  |-  ( ph  ->  C : NN --> ( RR 
^m  X ) )
1615ffvelrnda 6037 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  X
) )
17 elmapi 7511 . . . . . . 7  |-  ( ( C `  j )  e.  ( RR  ^m  X )  ->  ( C `  j ) : X --> RR )
1816, 17syl 17 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : X --> RR )
19 hspmbllem2.d . . . . . . . 8  |-  ( ph  ->  D : NN --> ( RR 
^m  X ) )
2019ffvelrnda 6037 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  X
) )
21 elmapi 7511 . . . . . . 7  |-  ( ( D `  j )  e.  ( RR  ^m  X )  ->  ( D `  j ) : X --> RR )
2220, 21syl 17 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : X --> RR )
2312, 14, 18, 22hoidmvcl 38522 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( D `  j ) )  e.  ( 0 [,) +oo ) )
2411, 23sseldi 3416 . . . 4  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( D `  j ) )  e.  ( 0 [,] +oo ) )
258, 10, 24sge0clmpt 38381 . . 3  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) ) )  e.  ( 0 [,] +oo ) )
26 hspmbllem2.k . . . . . . . . 9  |-  ( ph  ->  K  e.  X )
27 ne0i 3728 . . . . . . . . 9  |-  ( K  e.  X  ->  X  =/=  (/) )
2826, 27syl 17 . . . . . . . 8  |-  ( ph  ->  X  =/=  (/) )
2928adantr 472 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  X  =/=  (/) )
3012, 14, 29, 18, 22hoidmvn0val 38524 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( D `  j ) )  = 
prod_ k  e.  X  ( vol `  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) ) )
3130mpteq2dva 4482 . . . . 5  |-  ( ph  ->  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) )  =  ( j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) ) ) )
3231fveq2d 5883 . . . 4  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) ) )  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) ) ) ) )
33 hspmbllem2.g . . . 4  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) ) ) )  <_  ( (
(voln* `  X ) `  A
)  +  E ) )
3432, 33eqbrtrd 4416 . . 3  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) ) )  <_ 
( ( (voln* `  X ) `  A
)  +  E ) )
357, 25, 34ge0lere 37730 . 2  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) ) )  e.  RR )
36 hspmbllem2.t . . . . . . . . 9  |-  T  =  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) ) )
37 hspmbllem2.y . . . . . . . . . 10  |-  ( ph  ->  Y  e.  RR )
3837adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e.  RR )
3936, 38, 14, 22hsphoif 38516 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( T `  Y ) `
 ( D `  j ) ) : X --> RR )
4012, 14, 18, 39hoidmvcl 38522 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( ( T `
 Y ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
4111, 40sseldi 3416 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( ( T `
 Y ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
428, 10, 41sge0clmpt 38381 . . . . 5  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( ( T `  Y
) `  ( D `  j ) ) ) ) )  e.  ( 0 [,] +oo )
)
43 oveq2 6316 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( RR  ^m  x )  =  ( RR  ^m  y
) )
44 eqeq1 2475 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  =  (/)  <->  y  =  (/) ) )
45 prodeq1 14040 . . . . . . . . . . . 12  |-  ( x  =  y  ->  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) )  =  prod_ k  e.  y  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) )
4644, 45ifbieq2d 3897 . . . . . . . . . . 11  |-  ( x  =  y  ->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) ( b `  k ) ) ) )  =  if ( y  =  (/) ,  0 ,  prod_ k  e.  y  ( vol `  (
( a `  k
) [,) ( b `
 k ) ) ) ) )
4743, 43, 46mpt2eq123dv 6372 . . . . . . . . . 10  |-  ( x  =  y  ->  (
a  e.  ( RR 
^m  x ) ,  b  e.  ( RR 
^m  x )  |->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) )  =  ( a  e.  ( RR  ^m  y
) ,  b  e.  ( RR  ^m  y
)  |->  if ( y  =  (/) ,  0 , 
prod_ k  e.  y 
( vol `  (
( a `  k
) [,) ( b `
 k ) ) ) ) ) )
4847cbvmptv 4488 . . . . . . . . 9  |-  ( x  e.  Fin  |->  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x )  |->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) ( b `  k ) ) ) ) ) )  =  ( y  e.  Fin  |->  ( a  e.  ( RR  ^m  y ) ,  b  e.  ( RR  ^m  y ) 
|->  if ( y  =  (/) ,  0 ,  prod_ k  e.  y  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
4912, 48eqtri 2493 . . . . . . . 8  |-  L  =  ( y  e.  Fin  |->  ( a  e.  ( RR  ^m  y ) ,  b  e.  ( RR  ^m  y ) 
|->  if ( y  =  (/) ,  0 ,  prod_ k  e.  y  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
50 diffi 7821 . . . . . . . . . . 11  |-  ( X  e.  Fin  ->  ( X  \  { K }
)  e.  Fin )
5113, 50syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( X  \  { K } )  e.  Fin )
52 snfi 7668 . . . . . . . . . . 11  |-  { K }  e.  Fin
5352a1i 11 . . . . . . . . . 10  |-  ( ph  ->  { K }  e.  Fin )
54 unfi 7856 . . . . . . . . . 10  |-  ( ( ( X  \  { K } )  e.  Fin  /\ 
{ K }  e.  Fin )  ->  ( ( X  \  { K } )  u.  { K } )  e.  Fin )
5551, 53, 54syl2anc 673 . . . . . . . . 9  |-  ( ph  ->  ( ( X  \  { K } )  u. 
{ K } )  e.  Fin )
5655adantr 472 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( X  \  { K } )  u.  { K } )  e.  Fin )
57 snidg 3986 . . . . . . . . . . . 12  |-  ( K  e.  X  ->  K  e.  { K } )
5826, 57syl 17 . . . . . . . . . . 11  |-  ( ph  ->  K  e.  { K } )
59 elun2 3593 . . . . . . . . . . 11  |-  ( K  e.  { K }  ->  K  e.  ( ( X  \  { K } )  u.  { K } ) )
6058, 59syl 17 . . . . . . . . . 10  |-  ( ph  ->  K  e.  ( ( X  \  { K } )  u.  { K } ) )
61 neldifsnd 4091 . . . . . . . . . 10  |-  ( ph  ->  -.  K  e.  ( X  \  { K } ) )
6260, 61eldifd 3401 . . . . . . . . 9  |-  ( ph  ->  K  e.  ( ( ( X  \  { K } )  u.  { K } )  \  ( X  \  { K }
) ) )
6362adantr 472 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  K  e.  ( ( ( X 
\  { K }
)  u.  { K } )  \  ( X  \  { K }
) ) )
64 eqid 2471 . . . . . . . 8  |-  ( ( X  \  { K } )  u.  { K } )  =  ( ( X  \  { K } )  u.  { K } )
65 eqid 2471 . . . . . . . 8  |-  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u. 
{ K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u. 
{ K } ) 
|->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) ) )  =  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) )
66 uncom 3569 . . . . . . . . . . . . 13  |-  ( ( X  \  { K } )  u.  { K } )  =  ( { K }  u.  ( X  \  { K } ) )
6766a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X  \  { K } )  u. 
{ K } )  =  ( { K }  u.  ( X  \  { K } ) ) )
6826snssd 4108 . . . . . . . . . . . . 13  |-  ( ph  ->  { K }  C_  X )
69 undif 3839 . . . . . . . . . . . . 13  |-  ( { K }  C_  X  <->  ( { K }  u.  ( X  \  { K } ) )  =  X )
7068, 69sylib 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( { K }  u.  ( X  \  { K } ) )  =  X )
7167, 70eqtrd 2505 . . . . . . . . . . 11  |-  ( ph  ->  ( ( X  \  { K } )  u. 
{ K } )  =  X )
7271adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( X  \  { K } )  u.  { K } )  =  X )
7372feq2d 5725 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) : ( ( X 
\  { K }
)  u.  { K } ) --> RR  <->  ( C `  j ) : X --> RR ) )
7418, 73mpbird 240 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : ( ( X  \  { K } )  u. 
{ K } ) --> RR )
7572feq2d 5725 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j ) : ( ( X 
\  { K }
)  u.  { K } ) --> RR  <->  ( D `  j ) : X --> RR ) )
7622, 75mpbird 240 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : ( ( X  \  { K } )  u. 
{ K } ) --> RR )
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 38526 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  (
( X  \  { K } )  u.  { K } ) ) ( ( ( y  e.  RR  |->  ( c  e.  ( RR  ^m  (
( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) `  Y
) `  ( D `  j ) ) )  <_  ( ( C `
 j ) ( L `  ( ( X  \  { K } )  u.  { K } ) ) ( D `  j ) ) )
7871fveq2d 5883 . . . . . . . . . 10  |-  ( ph  ->  ( L `  (
( X  \  { K } )  u.  { K } ) )  =  ( L `  X
) )
79 eqidd 2472 . . . . . . . . . 10  |-  ( ph  ->  ( C `  j
)  =  ( C `
 j ) )
8036a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  T  =  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) )
8171oveq2d 6324 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( RR  ^m  (
( X  \  { K } )  u.  { K } ) )  =  ( RR  ^m  X
) )
8271mpteq1d 4477 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) )  =  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h
) ,  if ( ( c `  h
)  <_  y , 
( c `  h
) ,  y ) ) ) )
8381, 82mpteq12dv 4474 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) )  =  ( c  e.  ( RR  ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) )
8483eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) )  =  ( c  e.  ( RR 
^m  ( ( X 
\  { K }
)  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) )
8584mpteq2dv 4483 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) ) )  =  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) )
8680, 85eqtr2d 2506 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  RR  |->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) )  =  T )
8786fveq1d 5881 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  RR  |->  ( c  e.  ( RR  ^m  (
( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) `  Y
)  =  ( T `
 Y ) )
8887fveq1d 5881 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( y  e.  RR  |->  ( c  e.  ( RR  ^m  ( ( X  \  { K } )  u. 
{ K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u. 
{ K } ) 
|->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) ) ) `  Y ) `  ( D `  j )
)  =  ( ( T `  Y ) `
 ( D `  j ) ) )
8978, 79, 88oveq123d 6329 . . . . . . . . 9  |-  ( ph  ->  ( ( C `  j ) ( L `
 ( ( X 
\  { K }
)  u.  { K } ) ) ( ( ( y  e.  RR  |->  ( c  e.  ( RR  ^m  (
( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) `  Y
) `  ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  X ) ( ( T `  Y ) `  ( D `  j )
) ) )
9089adantr 472 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  (
( X  \  { K } )  u.  { K } ) ) ( ( ( y  e.  RR  |->  ( c  e.  ( RR  ^m  (
( X  \  { K } )  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) `  Y
) `  ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  X ) ( ( T `  Y ) `  ( D `  j )
) ) )
9178adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( L `
 ( ( X 
\  { K }
)  u.  { K } ) )  =  ( L `  X
) )
9291oveqd 6325 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  (
( X  \  { K } )  u.  { K } ) ) ( D `  j ) )  =  ( ( C `  j ) ( L `  X
) ( D `  j ) ) )
9390, 92breq12d 4408 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( C `  j
) ( L `  ( ( X  \  { K } )  u. 
{ K } ) ) ( ( ( y  e.  RR  |->  ( c  e.  ( RR 
^m  ( ( X 
\  { K }
)  u.  { K } ) )  |->  ( h  e.  ( ( X  \  { K } )  u.  { K } )  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) ) ) ) ) `  Y
) `  ( D `  j ) ) )  <_  ( ( C `
 j ) ( L `  ( ( X  \  { K } )  u.  { K } ) ) ( D `  j ) )  <->  ( ( C `
 j ) ( L `  X ) ( ( T `  Y ) `  ( D `  j )
) )  <_  (
( C `  j
) ( L `  X ) ( D `
 j ) ) ) )
9477, 93mpbid 215 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  X
) ( ( T `
 Y ) `  ( D `  j ) ) )  <_  (
( C `  j
) ( L `  X ) ( D `
 j ) ) )
958, 10, 41, 24, 94sge0lempt 38366 . . . . 5  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( ( T `  Y
) `  ( D `  j ) ) ) ) )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  X ) ( D `
 j ) ) ) ) )
9635, 42, 95ge0lere 37730 . . . 4  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( ( T `  Y
) `  ( D `  j ) ) ) ) )  e.  RR )
97 hspmbllem2.s . . . . . . . . . 10  |-  S  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  =  K ,  if ( x  <_  ( c `  h ) ,  ( c `  h ) ,  x ) ,  ( c `  h
) ) ) ) )
9897, 38, 14, 18hoidifhspf 38558 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( S `  Y ) `
 ( C `  j ) ) : X --> RR )
9912, 14, 98, 22hoidmvcl 38522 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( S `  Y
) `  ( C `  j ) ) ( L `  X ) ( D `  j
) )  e.  ( 0 [,) +oo )
)
100 eqid 2471 . . . . . . . 8  |-  ( j  e.  NN  |->  ( ( ( S `  Y
) `  ( C `  j ) ) ( L `  X ) ( D `  j
) ) )  =  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) )
10199, 100fmptd 6061 . . . . . . 7  |-  ( ph  ->  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) ) : NN --> ( 0 [,) +oo ) )
10211a1i 11 . . . . . . 7  |-  ( ph  ->  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )
103101, 102fssd 5750 . . . . . 6  |-  ( ph  ->  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) ) : NN --> ( 0 [,] +oo ) )
10410, 103sge0cl 38337 . . . . 5  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) ) )  e.  ( 0 [,] +oo )
)
10511, 99sseldi 3416 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( S `  Y
) `  ( C `  j ) ) ( L `  X ) ( D `  j
) )  e.  ( 0 [,] +oo )
)
10626adantr 472 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  K  e.  X )
10712, 14, 18, 22, 106, 97, 38hoidifhspdmvle 38560 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( S `  Y
) `  ( C `  j ) ) ( L `  X ) ( D `  j
) )  <_  (
( C `  j
) ( L `  X ) ( D `
 j ) ) )
1088, 10, 105, 24, 107sge0lempt 38366 . . . . 5  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) ) )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  X ) ( D `
 j ) ) ) ) )
10935, 104, 108ge0lere 37730 . . . 4  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( ( S `
 Y ) `  ( C `  j ) ) ( L `  X ) ( D `
 j ) ) ) )  e.  RR )
11037adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  l  e.  NN )  ->  Y  e.  RR )
11113adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  l  e.  NN )  ->  X  e. 
Fin )
112 eleq1 2537 . . . . . . . . . . . 12  |-  ( j  =  l  ->  (
j  e.  NN  <->  l  e.  NN ) )
113112anbi2d 718 . . . . . . . . . . 11  |-  ( j  =  l  ->  (
( ph  /\  j  e.  NN )  <->  ( ph  /\  l  e.  NN ) ) )
114 fveq2 5879 . . . . . . . . . . . 12  |-  ( j  =  l  ->  ( D `  j )  =  ( D `  l ) )
115114feq1d 5724 . . . . . . . . . . 11  |-  ( j  =  l  ->  (
( D `  j
) : X --> RR  <->  ( D `  l ) : X --> RR ) )
116113, 115imbi12d 327 . . . . . . . . . 10  |-  ( j  =  l  ->  (
( ( ph  /\  j  e.  NN )  ->  ( D `  j
) : X --> RR )  <-> 
( ( ph  /\  l  e.  NN )  ->  ( D `  l
) : X --> RR ) ) )
117116, 22chvarv 2120 . . . . . . . . 9  |-  ( (
ph  /\  l  e.  NN )  ->  ( D `
 l ) : X --> RR )
11836, 110, 111, 117hsphoif 38516 . . . . . . . 8  |-  ( (
ph  /\  l  e.  NN )  ->  ( ( T `  Y ) `
 ( D `  l ) ) : X --> RR )
119 reex 9648 . . . . . . . . . . . 12  |-  RR  e.  _V
120119a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  _V )
121120, 13jca 541 . . . . . . . . . 10  |-  ( ph  ->  ( RR  e.  _V  /\  X  e.  Fin )
)
122121adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  l  e.  NN )  ->  ( RR  e.  _V  /\  X  e.  Fin ) )
123 elmapg 7503 . . . . . . . . 9  |-  ( ( RR  e.  _V  /\  X  e.  Fin )  ->  ( ( ( T `
 Y ) `  ( D `  l ) )  e.  ( RR 
^m  X )  <->  ( ( T `  Y ) `  ( D `  l
) ) : X --> RR ) )
124122, 123syl 17 . . . . . . . 8  |-  ( (
ph  /\  l  e.  NN )  ->  ( ( ( T `  Y
) `  ( D `  l ) )  e.  ( RR  ^m  X
)  <->  ( ( T `
 Y ) `  ( D `  l ) ) : X --> RR ) )
125118, 124mpbird 240 . . . . . . 7  |-  ( (
ph  /\  l  e.  NN )  ->  ( ( T `  Y ) `
 ( D `  l ) )  e.  ( RR  ^m  X
) )
126 eqid 2471 . . . . . . 7  |-  ( l  e.  NN  |->  ( ( T `  Y ) `
 ( D `  l ) ) )  =  ( l  e.  NN  |->  ( ( T `
 Y ) `  ( D `  l ) ) )
127125, 126fmptd 6061 . . . . . 6  |-  ( ph  ->  ( l  e.  NN  |->  ( ( T `  Y ) `  ( D `  l )
) ) : NN --> ( RR  ^m  X ) )
128 simpl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  ->  ph )
129 elinel1 3610 . . . . . . . . . . . . 13  |-  ( f  e.  ( A  i^i  ( K ( H `  X ) Y ) )  ->  f  e.  A )
130129adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  ->  f  e.  A )
131 hspmbllem2.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
132131sselda 3418 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
133 eliun 4274 . . . . . . . . . . . . 13  |-  ( f  e.  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  <->  E. j  e.  NN  f  e.  X_ k  e.  X  ( ( ( C `  j ) `
 k ) [,) ( ( D `  j ) `  k
) ) )
134132, 133sylib 201 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A )  ->  E. j  e.  NN  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
135128, 130, 134syl2anc 673 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  ->  E. j  e.  NN  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
136128adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  /\  j  e.  NN )  ->  ph )
137 elinel2 3611 . . . . . . . . . . . . . . 15  |-  ( f  e.  ( A  i^i  ( K ( H `  X ) Y ) )  ->  f  e.  ( K ( H `  X ) Y ) )
138137adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  ->  f  e.  ( K ( H `
 X ) Y ) )
139138adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  /\  j  e.  NN )  ->  f  e.  ( K ( H `
 X ) Y ) )
140 simpr 468 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  ( A  i^i  ( K ( H `  X ) Y ) ) )  /\  j  e.  NN )  ->  j  e.  NN )
141 ixpfn 7546 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  ->  f  Fn  X )
142141adantl 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  ->  f  Fn  X )
143 nfv 1769 . . . . . . . . . . . . . . . . . 18  |-  F/ k ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )
144 nfcv 2612 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k
f
145 nfixp1 7560 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k X_ k  e.  X  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) )
146144, 145nfel 2624 . . . . . . . . . . . . . . . . . 18  |-  F/ k  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )
147143, 146nfan 2031 . . . . . . . . . . . . . . . . 17  |-  F/ k ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
148183adant3 1050 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( C `  j ) : X --> RR )
149 simp3 1032 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  k  e.  X )
150148, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( C `  j ) `  k )  e.  RR )
151150rexrd 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( C `  j ) `  k )  e.  RR* )
152151ad5ant135 1280 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  /\  k  e.  X )  ->  (
( C `  j
) `  k )  e.  RR* )
153393adant3 1050 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( T `  Y ) `  ( D `  j
) ) : X --> RR )
154153, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( (
( T `  Y
) `  ( D `  j ) ) `  k )  e.  RR )
155154rexrd 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( (
( T `  Y
) `  ( D `  j ) ) `  k )  e.  RR* )
156155ad5ant135 1280 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  /\  k  e.  X )  ->  (
( ( T `  Y ) `  ( D `  j )
) `  k )  e.  RR* )
157 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  K  ->  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  =  ( -oo (,) Y ) )
158 ioossre 11721 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -oo (,) Y )  C_  RR
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  K  ->  ( -oo (,) Y )  C_  RR )
160157, 159eqsstrd 3452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  K  ->  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  C_  RR )
161 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  k  =  K  ->  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  =  RR )
162 ssid 3437 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  C_  RR
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  k  =  K  ->  RR  C_  RR )
164161, 163eqsstrd 3452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  k  =  K  ->  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  C_  RR )
165160, 164pm2.61i 169 . . . . . . . . . . . . . . . . . . . . . 22  |-  if ( k  =  K , 
( -oo (,) Y ) ,  RR )  C_  RR
166 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  ->  f  e.  ( K ( H `  X ) Y ) )
167 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ k  e.  x  if ( k  =  l ,  ( -oo (,) y ) ,  RR ) ) )
168167, 13, 26, 37hspval 38549 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( K ( H `
 X ) Y )  =  X_ k  e.  X  if (
k  =  K , 
( -oo (,) Y ) ,  RR ) )
169168adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  ->  ( K
( H `  X
) Y )  = 
X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) )
170166, 169eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  ->  f  e.  X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) )
171170adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X )  ->  f  e.  X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) )
172 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X )  ->  k  e.  X )
173 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  f  e. 
_V
174173elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) 
<->  ( f  Fn  X  /\  A. k  e.  X  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR ) ) )
175174biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  e.  X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  ->  ( f  Fn  X  /\  A. k  e.  X  ( f `  k )  e.  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) ) )
176175simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  e.  X_ k  e.  X  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  ->  A. k  e.  X  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR ) )
177176adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  X_ k  e.  X  if (
k  =  K , 
( -oo (,) Y ) ,  RR )  /\  k  e.  X )  ->  A. k  e.  X  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR ) )
178 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  X_ k  e.  X  if (
k  =  K , 
( -oo (,) Y ) ,  RR )  /\  k  e.  X )  ->  k  e.  X )
179 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A. k  e.  X  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR )  /\  k  e.  X )  ->  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR ) )
180177, 178, 179syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  e.  X_ k  e.  X  if (
k  =  K , 
( -oo (,) Y ) ,  RR )  /\  k  e.  X )  ->  ( f `  k
)  e.  if ( k  =  K , 
( -oo (,) Y ) ,  RR ) )
181171, 172, 180syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X )  ->  (
f `  k )  e.  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) )
182165, 181sseldi 3416 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X )  ->  (
f `  k )  e.  RR )
183182rexrd 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X )  ->  (
f `  k )  e.  RR* )
184183ad4ant14 1259 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  /\  k  e.  X )  ->  (
f `  k )  e.  RR* )
185151ad4ant124 1261 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  X )  ->  ( ( C `  j ) `  k
)  e.  RR* )
186223adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( D `  j ) : X --> RR )
187186, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( D `  j ) `  k )  e.  RR )
188187rexrd 9708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( D `  j ) `  k )  e.  RR* )
189188ad4ant124 1261 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  X )  ->  ( ( D `  j ) `  k
)  e.  RR* )
190173elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  <->  ( f  Fn  X  /\  A. k  e.  X  ( f `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) ) )
191190biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  ->  ( f  Fn  X  /\  A. k  e.  X  ( f `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) ) )
192191simprd 470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  ->  A. k  e.  X  ( f `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
193192adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  X )  ->  A. k  e.  X  ( f `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
194 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  X )  ->  k  e.  X )
195 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A. k  e.  X  ( f `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  X )  ->  (
f `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
196193, 194, 195syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  X )  ->  (
f `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
197196adantll 728 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  X )  ->  ( f `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
198 icogelb 11711 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( C `  j ) `  k
)  e.  RR*  /\  (
( D `  j
) `  k )  e.  RR*  /\  ( f `
 k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  ->  (
( C `  j
) `  k )  <_  ( f `  k
) )
199185, 189, 197, 198syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  X )  ->  ( ( C `  j ) `  k
)  <_  ( f `  k ) )
200199ad5ant1345 1282 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  /\  k  e.  X )  ->  (
( C `  j
) `  k )  <_  ( f `  k
) )
201 icoltub 37703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( C `  j ) `  k
)  e.  RR*  /\  (
( D `  j
) `  k )  e.  RR*  /\  ( f `
 k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  ->  (
f `  k )  <  ( ( D `  j ) `  k
) )
202185, 189, 197, 201syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  X )  ->  ( f `  k
)  <  ( ( D `  j ) `  k ) )
203202ad5ant1345 1282 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )  /\  k  e.  X )  ->  (
f `  k )  <  ( ( D `  j ) `  k
) )
204203ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  k  =  K )  /\  (
( D `  j
) `  k )  <_  Y )  ->  (
f `  k )  <  ( ( D `  j ) `  k
) )
205 simpll 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  ->  ph )
206 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  ->  j  e.  NN )
207205, 206jca 541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  ->  ( ph  /\  j  e.  NN ) )
2082073ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  =  K  /\  ( ( D `
 j ) `  k )  <_  Y
)  ->  ( ph  /\  j  e.  NN ) )
209 simp2 1031 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  =  K  /\  ( ( D `
 j ) `  k )  <_  Y
)  ->  k  =  K )
210 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  =  K  /\  ( ( D `
 j ) `  k )  <_  Y
)  ->  ( ( D `  j ) `  k )  <_  Y
)
211 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  K  ->  (
( D `  j
) `  k )  =  ( ( D `
 j ) `  K ) )
212211breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  K  ->  (
( ( D `  j ) `  k
)  <_  Y  <->  ( ( D `  j ) `  K )  <_  Y
) )
213212biimpa 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  =  K  /\  ( ( D `  j ) `  k
)  <_  Y )  ->  ( ( D `  j ) `  K
)  <_  Y )
214213iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  =  K  /\  ( ( D `  j ) `  k
)  <_  Y )  ->  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
)  =  ( ( D `  j ) `
 K ) )
215211eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  K  ->  (
( D `  j
) `  K )  =  ( ( D `
 j ) `  k ) )
216215adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  =  K  /\  ( ( D `  j ) `  k
)  <_  Y )  ->  ( ( D `  j ) `  K
)  =  ( ( D `  j ) `
 k ) )
217214, 216eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( k  =  K  /\  ( ( D `  j ) `  k
)  <_  Y )  ->  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
)  =  ( ( D `  j ) `
 k ) )
2182173adant1 1048 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  j  e.  NN )  /\  k  =  K  /\  (
( D `  j
) `  k )  <_  Y )  ->  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
)  =  ( ( D `  j ) `
 k ) )
219 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  Y  ->  (
( c `  h
)  <_  y  <->  ( c `  h )  <_  Y
) )
220 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  Y  ->  y  =  Y )
221219, 220ifbieq2d 3897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  Y  ->  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y )  =  if ( ( c `  h
)  <_  Y , 
( c `  h
) ,  Y ) )
222221ifeq2d 3891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  Y  ->  if ( h  e.  ( X  \  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_ 
y ,  ( c `
 h ) ,  y ) )  =  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) )
223222mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  Y  ->  (
h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) )  =  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  Y ,  ( c `  h ) ,  Y
) ) ) )
224223mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  Y  ->  (
c  e.  ( RR 
^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) )  =  ( c  e.  ( RR 
^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) ) ) )
225224adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  y  =  Y )  ->  (
c  e.  ( RR 
^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  y ,  ( c `  h ) ,  y ) ) ) )  =  ( c  e.  ( RR 
^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) ) ) )
226 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
^m  X )  e. 
_V
227226mptex 6152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  ( RR  ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  Y ,  ( c `  h ) ,  Y
) ) ) )  e.  _V
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) ) )  e.  _V )
22980, 225, 37, 228fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( T `  Y
)  =  ( c  e.  ( RR  ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  Y ,  ( c `  h ) ,  Y
) ) ) ) )
230229adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 Y )  =  ( c  e.  ( RR  ^m  X ) 
|->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) ) ) )
231 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  ( D `  j )  ->  (
c `  h )  =  ( ( D `
 j ) `  h ) )
232231breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  ( D `  j )  ->  (
( c `  h
)  <_  Y  <->  ( ( D `  j ) `  h )  <_  Y
) )
233232, 231ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  ( D `  j )  ->  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y
)  =  if ( ( ( D `  j ) `  h
)  <_  Y , 
( ( D `  j ) `  h
) ,  Y ) )
234231, 233ifeq12d 3892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  ( D `  j )  ->  if ( h  e.  ( X  \  { K }
) ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  Y ,  ( c `  h ) ,  Y
) )  =  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) )
235234mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  ( D `  j )  ->  (
h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) )  =  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( ( D `  j ) `
 h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) )
236235adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  NN )  /\  c  =  ( D `  j ) )  -> 
( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( c `  h ) ,  if ( ( c `  h )  <_  Y ,  ( c `  h ) ,  Y ) ) )  =  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( ( D `  j ) `
 h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) )
237 mptexg 6151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( X  e.  Fin  ->  (
h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) )  e. 
_V )
23813, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) )  e. 
_V )
239238adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  NN )  ->  ( h  e.  X  |->  if ( h  e.  ( X 
\  { K }
) ,  ( ( D `  j ) `
 h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) )  e. 
_V )
240230, 236, 20, 239fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( T `  Y ) `
 ( D `  j ) )  =  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) )
241240fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( T `  Y
) `  ( D `  j ) ) `  k )  =  ( ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k ) )
2422413adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  NN  /\  k  =  K )  ->  ( (
( T `  Y
) `  ( D `  j ) ) `  k )  =  ( ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k ) )
243 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  k  =  K )  ->  ph )
244 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  =  K )  ->  k  =  K )
245243, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  =  K )  ->  K  e.  X )
246244, 245eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  k  =  K )  ->  k  e.  X )
247 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  e.  X )  ->  (
h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) )  =  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) )
248 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  k  ->  (
h  e.  ( X 
\  { K }
)  <->  k  e.  ( X  \  { K } ) ) )
249 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  k  ->  (
( D `  j
) `  h )  =  ( ( D `
 j ) `  k ) )
250249breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( h  =  k  ->  (
( ( D `  j ) `  h
)  <_  Y  <->  ( ( D `  j ) `  k )  <_  Y
) )
251250, 249ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  k  ->  if ( ( ( D `
 j ) `  h )  <_  Y ,  ( ( D `
 j ) `  h ) ,  Y
)  =  if ( ( ( D `  j ) `  k
)  <_  Y , 
( ( D `  j ) `  k
) ,  Y ) )
252248, 249, 251ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  =  k  ->  if ( h  e.  ( X  \  { K }
) ,  ( ( D `  j ) `
 h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
253252adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  k  e.  X )  /\  h  =  k )  ->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
254 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  e.  X )  ->  k  e.  X )
255 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( D `  j ) `
 k )  e. 
_V
256255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( ( D `  j ) `  k
)  e.  _V )
257 ifexg 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( D `  j ) `  k
)  e.  _V  /\  Y  e.  RR )  ->  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
)  e.  _V )
258256, 37, 257syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
)  e.  _V )
259 ifexg 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( D `  j ) `  k
)  e.  _V  /\  if ( ( ( D `
 j ) `  k )  <_  Y ,  ( ( D `
 j ) `  k ) ,  Y
)  e.  _V )  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  e.  _V )
260256, 258, 259syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  e.  _V )
261260adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  e.  X )  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  e.  _V )
262247, 253, 254, 261fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  k  e.  X )  ->  (
( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
263243, 246, 262syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  =  K )  ->  (
( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
264 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  K  ->  (
k  e.  ( X 
\  { K }
)  <->  K  e.  ( X  \  { K }
) ) )
265212, 211ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  K  ->  if ( ( ( D `
 j ) `  k )  <_  Y ,  ( ( D `
 j ) `  k ) ,  Y
)  =  if ( ( ( D `  j ) `  K
)  <_  Y , 
( ( D `  j ) `  K
) ,  Y ) )
266264, 211, 265ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  K  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  =  if ( K  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  K ) ,  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
) ) )
267266adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  =  K )  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  =  if ( K  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  K ) ,  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
) ) )
268263, 267eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  =  K )  ->  (
( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k )  =  if ( K  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  K ) ,  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
) ) )
2692683adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  NN  /\  k  =  K )  ->  ( (
h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) `  k )  =  if ( K  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  K ) ,  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
) ) )
270 neldifsnd 4091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  K  ->  -.  K  e.  ( X  \  { K } ) )
271270iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  K  ->  if ( K  e.  ( X  \  { K }
) ,  ( ( D `  j ) `
 K ) ,  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
) )  =  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
) )
2722713ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  NN  /\  k  =  K )  ->  if ( K  e.  ( X  \  { K } ) ,  ( ( D `
 j ) `  K ) ,  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
) )  =  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
) )
273242, 269, 2723eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  NN  /\  k  =  K )  ->  if (
( ( D `  j ) `  K
)  <_  Y , 
( ( D `  j ) `  K
) ,  Y )  =  ( ( ( T `  Y ) `
 ( D `  j ) ) `  k ) )
2742733expa 1231 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  j  e.  NN )  /\  k  =  K )  ->  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
)  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
2752743adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  j  e.  NN )  /\  k  =  K  /\  (
( D `  j
) `  k )  <_  Y )  ->  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
)  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
276218, 275eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  j  e.  NN )  /\  k  =  K  /\  (
( D `  j
) `  k )  <_  Y )  ->  (
( D `  j
) `  k )  =  ( ( ( T `  Y ) `
 ( D `  j ) ) `  k ) )
277208, 209, 210, 276syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  =  K  /\  ( ( D `
 j ) `  k )  <_  Y
)  ->  ( ( D `  j ) `  k )  =  ( ( ( T `  Y ) `  ( D `  j )
) `  k )
)
278277ad5ant145 1281 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  k  =  K )  /\  (
( D `  j
) `  k )  <_  Y )  ->  (
( D `  j
) `  k )  =  ( ( ( T `  Y ) `
 ( D `  j ) ) `  k ) )
279204, 278breqtrd 4420 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  k  =  K )  /\  (
( D `  j
) `  k )  <_  Y )  ->  (
f `  k )  <  ( ( ( T `
 Y ) `  ( D `  j ) ) `  k ) )
280 mnfxr 11437 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |- -oo  e.  RR*
281280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  -> -oo  e.  RR* )
28237rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  Y  e.  RR* )
283282adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  ->  Y  e.  RR* )
2842833ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  ->  Y  e.  RR* )
2851813adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  ->  (
f `  k )  e.  if ( k  =  K ,  ( -oo (,) Y ) ,  RR ) )
2861573ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  ->  if ( k  =  K ,  ( -oo (,) Y ) ,  RR )  =  ( -oo (,) Y ) )
287285, 286eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  ->  (
f `  k )  e.  ( -oo (,) Y
) )
288 iooltub 37706 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -oo  e.  RR*  /\  Y  e.  RR*  /\  ( f `
 k )  e.  ( -oo (,) Y
) )  ->  (
f `  k )  <  Y )
289281, 284, 287, 288syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  k  e.  X  /\  k  =  K )  ->  (
f `  k )  <  Y )
2902893adant1r 1285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  e.  X  /\  k  =  K
)  ->  ( f `  k )  <  Y
)
291290ad4ant123 1260 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  ( f `  k
)  <  Y )
292 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  -.  ( ( D `
 j ) `  k )  <_  Y
)
293212notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  K  ->  ( -.  ( ( D `  j ) `  k
)  <_  Y  <->  -.  (
( D `  j
) `  K )  <_  Y ) )
294293adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  ( -.  ( ( D `  j ) `
 k )  <_  Y 
<->  -.  ( ( D `
 j ) `  K )  <_  Y
) )
295292, 294mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  -.  ( ( D `
 j ) `  K )  <_  Y
)
296295iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
)  =  Y )
297 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  Y  =  Y )
298296, 297eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  =  K  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  Y  =  if ( ( ( D `  j ) `  K
)  <_  Y , 
( ( D `  j ) `  K
) ,  Y ) )
299298adantll 728 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  Y  =  if ( ( ( D `  j ) `  K
)  <_  Y , 
( ( D `  j ) `  K
) ,  Y ) )
300274adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  j  e.  NN )  /\  k  e.  X
)  /\  k  =  K )  ->  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
)  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
301300adantlllr 37424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  f  e.  ( K ( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  e.  X
)  /\  k  =  K )  ->  if ( ( ( D `
 j ) `  K )  <_  Y ,  ( ( D `
 j ) `  K ) ,  Y
)  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
302301adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  if ( ( ( D `  j ) `
 K )  <_  Y ,  ( ( D `  j ) `  K ) ,  Y
)  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
303299, 302eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  Y  =  ( ( ( T `  Y
) `  ( D `  j ) ) `  k ) )
304291, 303breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  ( f `  k
)  <  ( (
( T `  Y
) `  ( D `  j ) ) `  k ) )
305304ad5ant1345 1282 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ph  /\  f  e.  ( K ( H `
 X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  k  =  K )  /\  -.  ( ( D `  j ) `  k
)  <_  Y )  ->  ( f `  k
)  <  ( (
( T `  Y
) `  ( D `  j ) ) `  k ) )
306279, 305pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  k  =  K )  ->  (
f `  k )  <  ( ( ( T `
 Y ) `  ( D `  j ) ) `  k ) )
307203adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  -.  k  =  K )  ->  ( f `  k
)  <  ( ( D `  j ) `  k ) )
3082403adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( ( T `  Y ) `  ( D `  j
) )  =  ( h  e.  X  |->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) ) ) )
309252adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  j  e.  NN  /\  k  e.  X )  /\  h  =  k )  ->  if ( h  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  h ) ,  if ( ( ( D `  j ) `
 h )  <_  Y ,  ( ( D `  j ) `  h ) ,  Y
) )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
3102613adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  if (
k  e.  ( X 
\  { K }
) ,  ( ( D `  j ) `
 k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  e.  _V )
311308, 309, 149, 310fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN  /\  k  e.  X
)  ->  ( (
( T `  Y
) `  ( D `  j ) ) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
3123113expa 1231 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  j  e.  NN )  /\  k  e.  X )  ->  (
( ( T `  Y ) `  ( D `  j )
) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
313312adantllr 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f  e.  ( K
( H `  X
) Y ) )  /\  j  e.  NN )  /\  k  e.  X
)  ->  ( (
( T `  Y
) `  ( D `  j ) ) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) ) )
314313ad4ant13 1258 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  -.  k  =  K )  ->  ( ( ( T `
 Y ) `  ( D `  j ) ) `  k )  =  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j ) `  k
) ,  if ( ( ( D `  j ) `  k
)  <_  Y , 
( ( D `  j ) `  k
) ,  Y ) ) )
315 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  X  /\  -.  k  =  K
)  ->  k  e.  X )
316 neqne 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  k  =  K  -> 
k  =/=  K )
317 nelsn 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =/=  K  ->  -.  k  e.  { K } )
318316, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  k  =  K  ->  -.  k  e.  { K } )
319318adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  X  /\  -.  k  =  K
)  ->  -.  k  e.  { K } )
320315, 319eldifd 3401 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( k  e.  X  /\  -.  k  =  K
)  ->  k  e.  ( X  \  { K } ) )
321320iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  X  /\  -.  k  =  K
)  ->  if (
k  e.  ( X 
\  { K }
) ,  ( ( D `  j ) `
 k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  =  ( ( D `  j
) `  k )
)
322321adantll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k  e.  X )  /\  -.  k  =  K )  ->  if ( k  e.  ( X  \  { K } ) ,  ( ( D `  j
) `  k ) ,  if ( ( ( D `  j ) `
 k )  <_  Y ,  ( ( D `  j ) `  k ) ,  Y
) )  =  ( ( D `  j
) `  k )
)
323314, 322eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  f  e.  ( K ( H `  X ) Y ) )  /\  j  e.  NN )  /\  f  e.  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  /\  k