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

Theorem hoidmvlelem3 38537
Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem3.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 )
) ) ) ) )
hoidmvlelem3.x  |-  ( ph  ->  X  e.  Fin )
hoidmvlelem3.y  |-  ( ph  ->  Y  C_  X )
hoidmvlelem3.z  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
hoidmvlelem3.w  |-  W  =  ( Y  u.  { Z } )
hoidmvlelem3.a  |-  ( ph  ->  A : W --> RR )
hoidmvlelem3.b  |-  ( ph  ->  B : W --> RR )
hoidmvlelem3.lt  |-  ( (
ph  /\  k  e.  W )  ->  ( A `  k )  <  ( B `  k
) )
hoidmvlelem3.f  |-  F  =  ( y  e.  Y  |->  0 )
hoidmvlelem3.c  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
hoidmvlelem3.j  |-  J  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) )
hoidmvlelem3.d  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
hoidmvlelem3.k  |-  K  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) )
hoidmvlelem3.r  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
hoidmvlelem3.h  |-  H  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W ) 
|->  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) ) )
hoidmvlelem3.g  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
hoidmvlelem3.e  |-  ( ph  ->  E  e.  RR+ )
hoidmvlelem3.u  |-  U  =  { z  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  |  ( G  x.  ( z  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) }
hoidmvlelem3.s  |-  ( ph  ->  S  e.  U )
hoidmvlelem3.sb  |-  ( ph  ->  S  <  ( B `
 Z ) )
hoidmvlelem3.p  |-  P  =  ( j  e.  NN  |->  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
hoidmvlelem3.i  |-  ( ph  ->  A. e  e.  ( RR  ^m  Y ) A. f  e.  ( RR  ^m  Y ) A. g  e.  ( ( RR  ^m  Y
)  ^m  NN ) A. h  e.  (
( RR  ^m  Y
)  ^m  NN )
( X_ k  e.  Y  ( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  Y  ( ( ( g `
 j ) `  k ) [,) (
( h `  j
) `  k )
)  ->  ( e
( L `  Y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( g `  j ) ( L `
 Y ) ( h `  j ) ) ) ) ) )
hoidmvlelem3.i2  |-  ( ph  -> 
X_ k  e.  W  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
hoidmvlelem3.o  |-  O  =  ( x  e.  X_ k  e.  Y  (
( A `  k
) [,) ( B `
 k ) ) 
|->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) )
Assertion
Ref Expression
hoidmvlelem3  |-  ( ph  ->  E. u  e.  U  S  <  u )
Distinct variable groups:    A, a,
b, h, j, k, x    A, e, f, g, h, j, k    z, A, h, j    B, a, b, h, j, k, x, y    B, c, h, j, k, x    B, f, g    u, B, h, j    z, B    C, a, b, h, j, k, x, y    C, c    u, C    z, C    D, a, b, h, j, k, x, y    D, c    u, D    z, D    E, a, b, h, k, x, y    E, c   
z, E    j, F    G, a, b, h, k, x, y    G, c   
z, G    H, a,
b, j, k    z, H    J, a, b, h, j, k, x    g, J    K, a, b, h, j, k, x    L, a, b, h, j, k, x    e, L, f, g    z, L    j, O, k    P, a, b, h, j, k, x, y    P, c    S, a, b, h, j, k, x, y    S, c   
u, S    z, S    u, U    W, a, b, j, k, x    W, c   
z, W    Y, a,
b, h, j, k, x, y    Y, c   
e, Y, f, g    Z, a, b, h, j, k, x, y    Z, c    u, Z    z, Z    ph, a, b, h, j, k, x, y    ph, c
Allowed substitution hints:    ph( z, u, e, f, g)    A( y, u, c)    B( e)    C( e, f, g)    D( e, f, g)    P( z, u, e, f, g)    S( e, f, g)    U( x, y, z, e, f, g, h, j, k, a, b, c)    E( u, e, f, g, j)    F( x, y, z, u, e, f, g, h, k, a, b, c)    G( u, e, f, g, j)    H( x, y, u, e, f, g, h, c)    J( y, z, u, e, f, c)    K( y, z, u, e, f, g, c)    L( y, u, c)    O( x, y, z, u, e, f, g, h, a, b, c)    W( y, u, e, f, g, h)    X( x, y, z, u, e, f, g, h, j, k, a, b, c)    Y( z, u)    Z( e, f, g)

Proof of Theorem hoidmvlelem3
Dummy variables  i  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 10642 . . . . 5  |-  1  e.  NN
21a1i 11 . . . 4  |-  ( (
ph  /\  Y  =  (/) )  ->  1  e.  NN )
3 0le0 10721 . . . . . 6  |-  0  <_  0
43a1i 11 . . . . 5  |-  ( (
ph  /\  Y  =  (/) )  ->  0  <_  0 )
5 hoidmvlelem3.g . . . . . . . 8  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
65a1i 11 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
) )
7 fveq2 5879 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( L `
 Y )  =  ( L `  (/) ) )
8 reseq2 5106 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( A  |`  Y )  =  ( A  |`  (/) ) )
9 res0 5115 . . . . . . . . . . 11  |-  ( A  |`  (/) )  =  (/)
109a1i 11 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( A  |`  (/) )  =  (/) )
118, 10eqtrd 2505 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( A  |`  Y )  =  (/) )
12 reseq2 5106 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( B  |`  Y )  =  ( B  |`  (/) ) )
13 res0 5115 . . . . . . . . . . 11  |-  ( B  |`  (/) )  =  (/)
1413a1i 11 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( B  |`  (/) )  =  (/) )
1512, 14eqtrd 2505 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( B  |`  Y )  =  (/) )
167, 11, 15oveq123d 6329 . . . . . . . 8  |-  ( Y  =  (/)  ->  ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  =  ( (/) ( L `  (/) ) (/) ) )
1716adantl 473 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( A  |`  Y ) ( L `  Y ) ( B  |`  Y ) )  =  ( (/) ( L `  (/) ) (/) ) )
18 hoidmvlelem3.l . . . . . . . 8  |-  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 )
) ) ) ) )
19 f0 5777 . . . . . . . . 9  |-  (/) : (/) --> RR
2019a1i 11 . . . . . . . 8  |-  ( (
ph  /\  Y  =  (/) )  ->  (/) : (/) --> RR )
2118, 20, 20hoidmv0val 38523 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (/) ( L `
 (/) ) (/) )  =  0 )
226, 17, 213eqtrd 2509 . . . . . 6  |-  ( (
ph  /\  Y  =  (/) )  ->  G  = 
0 )
23 nfcvd 2613 . . . . . . . . . . 11  |-  ( ph  -> 
F/_ j ( P `
 1 ) )
24 nfv 1769 . . . . . . . . . . 11  |-  F/ j
ph
25 simpr 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  = 
1 )  ->  j  =  1 )
2625fveq2d 5883 . . . . . . . . . . 11  |-  ( (
ph  /\  j  = 
1 )  ->  ( P `  j )  =  ( P ` 
1 ) )
27 1red 9676 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  RR )
28 rge0ssre 11766 . . . . . . . . . . . . 13  |-  ( 0 [,) +oo )  C_  RR
29 id 22 . . . . . . . . . . . . . 14  |-  ( ph  ->  ph )
301a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  NN )
311elexi 3041 . . . . . . . . . . . . . . 15  |-  1  e.  _V
32 eleq1 2537 . . . . . . . . . . . . . . . . 17  |-  ( j  =  1  ->  (
j  e.  NN  <->  1  e.  NN ) )
3332anbi2d 718 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( ph  /\  j  e.  NN )  <->  ( ph  /\  1  e.  NN ) ) )
34 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( j  =  1  ->  ( P `  j )  =  ( P ` 
1 ) )
3534eleq1d 2533 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( P `  j
)  e.  ( 0 [,) +oo )  <->  ( P `  1 )  e.  ( 0 [,) +oo ) ) )
3633, 35imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( j  =  1  ->  (
( ( ph  /\  j  e.  NN )  ->  ( P `  j
)  e.  ( 0 [,) +oo ) )  <-> 
( ( ph  /\  1  e.  NN )  ->  ( P `  1
)  e.  ( 0 [,) +oo ) ) ) )
37 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  NN  ->  j  e.  NN )
38 ovex 6336 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e. 
_V
3938a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  NN  ->  (
( J `  j
) ( L `  Y ) ( K `
 j ) )  e.  _V )
40 hoidmvlelem3.p . . . . . . . . . . . . . . . . . . 19  |-  P  =  ( j  e.  NN  |->  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
4140fvmpt2 5972 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  NN  /\  ( ( J `  j ) ( L `
 Y ) ( K `  j ) )  e.  _V )  ->  ( P `  j
)  =  ( ( J `  j ) ( L `  Y
) ( K `  j ) ) )
4237, 39, 41syl2anc 673 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  NN  ->  ( P `  j )  =  ( ( J `
 j ) ( L `  Y ) ( K `  j
) ) )
4342adantl 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  =  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
44 hoidmvlelem3.x . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  Fin )
45 hoidmvlelem3.w . . . . . . . . . . . . . . . . . . . . . 22  |-  W  =  ( Y  u.  { Z } )
4645a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  W  =  ( Y  u.  { Z }
) )
47 hoidmvlelem3.y . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Y  C_  X )
48 hoidmvlelem3.z . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
4948eldifad 3402 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  Z  e.  X )
50 snssi 4107 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Z  e.  X  ->  { Z }  C_  X )
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  { Z }  C_  X )
5247, 51unssd 3601 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Y  u.  { Z } )  C_  X
)
5346, 52eqsstrd 3452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  W  C_  X )
5444, 53ssfid 37473 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  W  e.  Fin )
55 ssun1 3588 . . . . . . . . . . . . . . . . . . . . 21  |-  Y  C_  ( Y  u.  { Z } )
5645eqcomi 2480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Y  u.  { Z }
)  =  W
5755, 56sseqtri 3450 . . . . . . . . . . . . . . . . . . . 20  |-  Y  C_  W
5857a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  C_  W )
5954, 58ssfid 37473 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Y  e.  Fin )
6059adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
Fin )
61 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  ( ( C `  j )  |`  Y ) )
6261adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  ( ( C `  j )  |`  Y ) )
63 hoidmvlelem3.c . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
6463ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
65 elmapi 7511 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( C `  j )  e.  ( RR  ^m  W )  ->  ( C `  j ) : W --> RR )
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : W --> RR )
6755, 45sseqtr4i 3451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  Y  C_  W
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  Y  C_  W )
6966, 68fssresd 5762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y ) : Y --> RR )
70 reex 9648 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  e.  _V
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  RR  e.  _V )
7254, 58ssexd 4543 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  Y  e.  _V )
7372adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
_V )
7471, 73elmapd 7504 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( C `  j
)  |`  Y )  e.  ( RR  ^m  Y
)  <->  ( ( C `
 j )  |`  Y ) : Y --> RR ) )
7569, 74mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y )  e.  ( RR  ^m  Y ) )
7675adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y )  e.  ( RR  ^m  Y
) )
7762, 76eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  ( RR 
^m  Y ) )
78 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
7978adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
80 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  Y )  ->  0  e.  RR )
81 hoidmvlelem3.f . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F  =  ( y  e.  Y  |->  0 )
8280, 81fmptd 6061 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : Y --> RR )
8370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  RR  e.  _V )
8483, 59elmapd 7504 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( F  e.  ( RR  ^m  Y )  <-> 
F : Y --> RR ) )
8582, 84mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  e.  ( RR 
^m  Y ) )
8685ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F  e.  ( RR  ^m  Y ) )
8779, 86eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  ( RR 
^m  Y ) )
8877, 87pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F )  e.  ( RR  ^m  Y ) )
89 hoidmvlelem3.j . . . . . . . . . . . . . . . . . . . 20  |-  J  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) )
9088, 89fmptd 6061 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  J : NN --> ( RR 
^m  Y ) )
9190ffvelrnda 6037 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  e.  ( RR  ^m  Y
) )
92 elmapi 7511 . . . . . . . . . . . . . . . . . 18  |-  ( ( J `  j )  e.  ( RR  ^m  Y )  ->  ( J `  j ) : Y --> RR )
9391, 92syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j ) : Y --> RR )
94 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  ( ( D `  j )  |`  Y ) )
9594adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  ( ( D `  j )  |`  Y ) )
96 hoidmvlelem3.d . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
9796ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
98 elmapi 7511 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( D `  j )  e.  ( RR  ^m  W )  ->  ( D `  j ) : W --> RR )
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : W --> RR )
10099, 68fssresd 5762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y ) : Y --> RR )
10171, 73elmapd 7504 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( D `  j
)  |`  Y )  e.  ( RR  ^m  Y
)  <->  ( ( D `
 j )  |`  Y ) : Y --> RR ) )
102100, 101mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y )  e.  ( RR  ^m  Y ) )
103102adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( D `  j
)  |`  Y )  e.  ( RR  ^m  Y
) )
10495, 103eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  e.  ( RR 
^m  Y ) )
105 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
106105adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
107106, 86eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  e.  ( RR 
^m  Y ) )
108104, 107pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F )  e.  ( RR  ^m  Y ) )
109 hoidmvlelem3.k . . . . . . . . . . . . . . . . . . . 20  |-  K  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) )
110108, 109fmptd 6061 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K : NN --> ( RR 
^m  Y ) )
111110ffvelrnda 6037 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j )  e.  ( RR  ^m  Y
) )
112 elmapi 7511 . . . . . . . . . . . . . . . . . 18  |-  ( ( K `  j )  e.  ( RR  ^m  Y )  ->  ( K `  j ) : Y --> RR )
113111, 112syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j ) : Y --> RR )
11418, 60, 93, 113hoidmvcl 38522 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e.  ( 0 [,) +oo ) )
11543, 114eqeltrd 2549 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,) +oo ) )
11631, 36, 115vtocl 3086 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( P `
 1 )  e.  ( 0 [,) +oo ) )
11729, 30, 116syl2anc 673 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P `  1
)  e.  ( 0 [,) +oo ) )
11828, 117sseldi 3416 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  1
)  e.  RR )
119118recnd 9687 . . . . . . . . . . 11  |-  ( ph  ->  ( P `  1
)  e.  CC )
12023, 24, 26, 27, 119sumsnd 37410 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  {
1 }  ( P `
 j )  =  ( P `  1
) )
121120adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  Y  =  (/) )  ->  sum_ j  e. 
{ 1 }  ( P `  j )  =  ( P ` 
1 ) )
122 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  1  ->  ( J `  j )  =  ( J ` 
1 ) )
123 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  1  ->  ( K `  j )  =  ( K ` 
1 ) )
124122, 123oveq12d 6326 . . . . . . . . . . . 12  |-  ( j  =  1  ->  (
( J `  j
) ( L `  Y ) ( K `
 j ) )  =  ( ( J `
 1 ) ( L `  Y ) ( K `  1
) ) )
125 ovex 6336 . . . . . . . . . . . 12  |-  ( ( J `  1 ) ( L `  Y
) ( K ` 
1 ) )  e. 
_V
126124, 40, 125fvmpt 5963 . . . . . . . . . . 11  |-  ( 1  e.  NN  ->  ( P `  1 )  =  ( ( J `
 1 ) ( L `  Y ) ( K `  1
) ) )
1271, 126ax-mp 5 . . . . . . . . . 10  |-  ( P `
 1 )  =  ( ( J ` 
1 ) ( L `
 Y ) ( K `  1 ) )
128127a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  Y  =  (/) )  ->  ( P `  1 )  =  ( ( J ` 
1 ) ( L `
 Y ) ( K `  1 ) ) )
1297oveqd 6325 . . . . . . . . . . 11  |-  ( Y  =  (/)  ->  ( ( J `  1 ) ( L `  Y
) ( K ` 
1 ) )  =  ( ( J ` 
1 ) ( L `
 (/) ) ( K `
 1 ) ) )
130129adantl 473 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  Y
) ( K ` 
1 ) )  =  ( ( J ` 
1 ) ( L `
 (/) ) ( K `
 1 ) ) )
131122feq1d 5724 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( J `  j
) : Y --> RR  <->  ( J `  1 ) : Y --> RR ) )
13233, 131imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( j  =  1  ->  (
( ( ph  /\  j  e.  NN )  ->  ( J `  j
) : Y --> RR )  <-> 
( ( ph  /\  1  e.  NN )  ->  ( J `  1
) : Y --> RR ) ) )
13369adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y ) : Y --> RR )
13462feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  ( if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR  <->  ( ( C `  j )  |`  Y ) : Y --> RR ) )
135133, 134mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR )
13682ad2antrr 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F : Y --> RR )
13779feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  -> 
( if ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR 
<->  F : Y --> RR ) )
138136, 137mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR )
139135, 138pm2.61dan 808 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR )
140 simpr 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
141 fvex 5889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( C `
 j )  e. 
_V
142141resex 5154 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C `  j )  |`  Y )  e.  _V
14362, 142syl6eqel 2557 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  _V )
14485elexd 3042 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F  e.  _V )
145144adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  NN )  ->  F  e. 
_V )
146145adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F  e.  _V )
14779, 146eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  _V )
148143, 147pm2.61dan 808 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F )  e.  _V )
14989fvmpt2 5972 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  NN  /\  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  _V )  ->  ( J `  j
)  =  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) )
150140, 148, 149syl2anc 673 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
) )
151150feq1d 5724 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) : Y --> RR  <->  if ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR ) )
152139, 151mpbird 240 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j ) : Y --> RR )
15331, 132, 152vtocl 3086 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( J `
 1 ) : Y --> RR )
15429, 30, 153syl2anc 673 . . . . . . . . . . . . 13  |-  ( ph  ->  ( J `  1
) : Y --> RR )
155154adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( J `  1 ) : Y --> RR )
156 id 22 . . . . . . . . . . . . . . 15  |-  ( Y  =  (/)  ->  Y  =  (/) )
157156eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( Y  =  (/)  ->  (/)  =  Y )
158157feq2d 5725 . . . . . . . . . . . . 13  |-  ( Y  =  (/)  ->  ( ( J `  1 ) : (/) --> RR  <->  ( J `  1 ) : Y --> RR ) )
159158adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 ) : (/) --> RR  <->  ( J `  1 ) : Y --> RR ) )
160155, 159mpbird 240 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =  (/) )  ->  ( J `  1 ) :
(/) --> RR )
161123feq1d 5724 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( K `  j
) : Y --> RR  <->  ( K `  1 ) : Y --> RR ) )
16233, 161imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( j  =  1  ->  (
( ( ph  /\  j  e.  NN )  ->  ( K `  j
) : Y --> RR )  <-> 
( ( ph  /\  1  e.  NN )  ->  ( K `  1
) : Y --> RR ) ) )
16331, 162, 113vtocl 3086 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( K `
 1 ) : Y --> RR )
16429, 30, 163syl2anc 673 . . . . . . . . . . . . 13  |-  ( ph  ->  ( K `  1
) : Y --> RR )
165164adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( K `  1 ) : Y --> RR )
166157feq2d 5725 . . . . . . . . . . . . 13  |-  ( Y  =  (/)  ->  ( ( K `  1 ) : (/) --> RR  <->  ( K `  1 ) : Y --> RR ) )
167166adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( K `  1 ) : (/) --> RR  <->  ( K `  1 ) : Y --> RR ) )
168165, 167mpbird 240 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =  (/) )  ->  ( K `  1 ) :
(/) --> RR )
16918, 160, 168hoidmv0val 38523 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  (/) ) ( K `  1 ) )  =  0 )
170130, 169eqtrd 2505 . . . . . . . . 9  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  Y
) ( K ` 
1 ) )  =  0 )
171121, 128, 1703eqtrd 2509 . . . . . . . 8  |-  ( (
ph  /\  Y  =  (/) )  ->  sum_ j  e. 
{ 1 }  ( P `  j )  =  0 )
172171oveq2d 6324 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (
1  +  E )  x.  sum_ j  e.  {
1 }  ( P `
 j ) )  =  ( ( 1  +  E )  x.  0 ) )
173 hoidmvlelem3.e . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
174173rpred 11364 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
17527, 174readdcld 9688 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
176175recnd 9687 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  E
)  e.  CC )
177176mul01d 9850 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  0 )  =  0 )
178177adantr 472 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (
1  +  E )  x.  0 )  =  0 )
179 eqidd 2472 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  0  = 
0 )
180172, 178, 1793eqtrd 2509 . . . . . 6  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (
1  +  E )  x.  sum_ j  e.  {
1 }  ( P `
 j ) )  =  0 )
18122, 180breq12d 4408 . . . . 5  |-  ( (
ph  /\  Y  =  (/) )  ->  ( G  <_  ( ( 1  +  E )  x.  sum_ j  e.  { 1 }  ( P `  j ) )  <->  0  <_  0 ) )
1824, 181mpbird 240 . . . 4  |-  ( (
ph  /\  Y  =  (/) )  ->  G  <_  ( ( 1  +  E
)  x.  sum_ j  e.  { 1 }  ( P `  j )
) )
183 oveq2 6316 . . . . . . . . 9  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
1841nnzi 10985 . . . . . . . . . . 11  |-  1  e.  ZZ
185 fzsn 11866 . . . . . . . . . . 11  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
186184, 185ax-mp 5 . . . . . . . . . 10  |-  ( 1 ... 1 )  =  { 1 }
187186a1i 11 . . . . . . . . 9  |-  ( m  =  1  ->  (
1 ... 1 )  =  { 1 } )
188183, 187eqtrd 2505 . . . . . . . 8  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
189188sumeq1d 13844 . . . . . . 7  |-  ( m  =  1  ->  sum_ j  e.  ( 1 ... m
) ( P `  j )  =  sum_ j  e.  { 1 }  ( P `  j ) )
190189oveq2d 6324 . . . . . 6  |-  ( m  =  1  ->  (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... m
) ( P `  j ) )  =  ( ( 1  +  E )  x.  sum_ j  e.  { 1 }  ( P `  j ) ) )
191190breq2d 4407 . . . . 5  |-  ( m  =  1  ->  ( G  <_  ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... m ) ( P `  j
) )  <->  G  <_  ( ( 1  +  E
)  x.  sum_ j  e.  { 1 }  ( P `  j )
) ) )
192191rspcev 3136 . . . 4  |-  ( ( 1  e.  NN  /\  G  <_  ( ( 1  +  E )  x. 
sum_ j  e.  {
1 }  ( P `
 j ) ) )  ->  E. m  e.  NN  G  <_  (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... m
) ( P `  j ) ) )
1932, 182, 192syl2anc 673 . . 3  |-  ( (
ph  /\  Y  =  (/) )  ->  E. m  e.  NN  G  <_  (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... m
) ( P `  j ) ) )
194 simpl 464 . . . 4  |-  ( (
ph  /\  -.  Y  =  (/) )  ->  ph )
195 neqne 2651 . . . . 5  |-  ( -.  Y  =  (/)  ->  Y  =/=  (/) )
196195adantl 473 . . . 4  |-  ( (
ph  /\  -.  Y  =  (/) )  ->  Y  =/=  (/) )
197 nfv 1769 . . . . . 6  |-  F/ j ( ph  /\  Y  =/=  (/) )
198184a1i 11 . . . . . 6  |-  ( (
ph  /\  Y  =/=  (/) )  ->  1  e.  ZZ )
199 nnuz 11218 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
200115adantlr 729 . . . . . 6  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  j  e.  NN )  ->  ( P `  j )  e.  ( 0 [,) +oo ) )
201 hoidmvlelem3.a . . . . . . . . . . . 12  |-  ( ph  ->  A : W --> RR )
20267a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Y  C_  W )
203201, 202fssresd 5762 . . . . . . . . . . 11  |-  ( ph  ->  ( A  |`  Y ) : Y --> RR )
204 hoidmvlelem3.b . . . . . . . . . . . 12  |-  ( ph  ->  B : W --> RR )
205204, 202fssresd 5762 . . . . . . . . . . 11  |-  ( ph  ->  ( B  |`  Y ) : Y --> RR )
20618, 59, 203, 205hoidmvcl 38522 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  ( 0 [,) +oo ) )
20728, 206sseldi 3416 . . . . . . . . 9  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  RR )
2085, 207syl5eqel 2553 . . . . . . . 8  |-  ( ph  ->  G  e.  RR )
209 0red 9662 . . . . . . . . 9  |-  ( ph  ->  0  e.  RR )
210 1rp 11329 . . . . . . . . . . . . 13  |-  1  e.  RR+
211210a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  RR+ )
212211, 173jca 541 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  e.  RR+  /\  E  e.  RR+ )
)
213 rpaddcl 11346 . . . . . . . . . . 11  |-  ( ( 1  e.  RR+  /\  E  e.  RR+ )  ->  (
1  +  E )  e.  RR+ )
214212, 213syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  E
)  e.  RR+ )
215 rpgt0 11336 . . . . . . . . . 10  |-  ( ( 1  +  E )  e.  RR+  ->  0  < 
( 1  +  E
) )
216214, 215syl 17 . . . . . . . . 9  |-  ( ph  ->  0  <  ( 1  +  E ) )
217209, 216gtned 9787 . . . . . . . 8  |-  ( ph  ->  ( 1  +  E
)  =/=  0 )
218208, 175, 217redivcld 10457 . . . . . . 7  |-  ( ph  ->  ( G  /  (
1  +  E ) )  e.  RR )
219218adantr 472 . . . . . 6  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( G  /  ( 1  +  E ) )  e.  RR )
220218ltpnfd 11446 . . . . . . . . . 10  |-  ( ph  ->  ( G  /  (
1  +  E ) )  < +oo )
221220adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( G  / 
( 1  +  E
) )  < +oo )
222 id 22 . . . . . . . . . . 11  |-  ( (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )
223222eqcomd 2477 . . . . . . . . . 10  |-  ( (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo  -> +oo  =  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) ) )
224223adantl 473 . . . . . . . . 9  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  -> +oo  =  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
225221, 224breqtrd 4420 . . . . . . . 8  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( G  / 
( 1  +  E
) )  <  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
226225adantlr 729 . . . . . . 7  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( G  / 
( 1  +  E
) )  <  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
227 simpl 464 . . . . . . . 8  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( ph  /\  Y  =/=  (/) ) )
228 simpr 468 . . . . . . . . . 10  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )
229 nnex 10637 . . . . . . . . . . . 12  |-  NN  e.  _V
230229a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  NN  e.  _V )
231 icossicc 11746 . . . . . . . . . . . . . 14  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
232231, 115sseldi 3416 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,] +oo ) )
233 eqid 2471 . . . . . . . . . . . . 13  |-  ( j  e.  NN  |->  ( P `
 j ) )  =  ( j  e.  NN  |->  ( P `  j ) )
234232, 233fmptd 6061 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  e.  NN  |->  ( P `  j ) ) : NN --> ( 0 [,] +oo ) )
235234adantr 472 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( j  e.  NN  |->  ( P `  j ) ) : NN --> ( 0 [,] +oo ) )
236230, 235sge0repnf 38342 . . . . . . . . . 10  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR  <->  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo ) )
237228, 236mpbird 240 . . . . . . . . 9  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
238237adantlr 729 . . . . . . . 8  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
239219adantr 472 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  ( G  / 
( 1  +  E
) )  e.  RR )
240208adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  G  e.  RR )
241240adantlr 729 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  G  e.  RR )
242 simpr 468 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
24327, 173ltaddrpd 11394 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  ( 1  +  E ) )
244243adantr 472 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =/=  (/) )  ->  1  <  ( 1  +  E ) )
24559adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  Y  e.  Fin )
246 simpr 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  Y  =/=  (/) )
247203adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( A  |`  Y ) : Y --> RR )
248205adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( B  |`  Y ) : Y --> RR )
24918, 245, 246, 247, 248hoidmvn0val 38524 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( ( A  |`  Y ) ( L `  Y ) ( B  |`  Y ) )  =  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) ) ) )
2505a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  Y  =/=  (/) )  ->  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
) )
251 fvres 5893 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  (
( A  |`  Y ) `
 k )  =  ( A `  k
) )
252 fvres 5893 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  (
( B  |`  Y ) `
 k )  =  ( B `  k
) )
253251, 252oveq12d 6326 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  Y  ->  (
( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) )  =  ( ( A `  k ) [,) ( B `  k )
) )
254253fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  Y  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( vol `  ( ( A `  k ) [,) ( B `  k )
) ) )
255254adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  Y )  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( vol `  ( ( A `  k ) [,) ( B `  k )
) ) )
256201adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  A : W --> RR )
257 elun1 3592 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  Y  ->  k  e.  ( Y  u.  { Z } ) )
258257, 45syl6eleqr 2560 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  k  e.  W )
259258adantl 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  k  e.  W )
260256, 259ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( A `  k )  e.  RR )
261204adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  B : W --> RR )
262261, 259ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( B `  k )  e.  RR )
263 volico 37958 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A `  k
)  e.  RR  /\  ( B `  k )  e.  RR )  -> 
( vol `  (
( A `  k
) [,) ( B `
 k ) ) )  =  if ( ( A `  k
)  <  ( B `  k ) ,  ( ( B `  k
)  -  ( A `
 k ) ) ,  0 ) )
264260, 262, 263syl2anc 673 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  Y )  ->  ( vol `  ( ( A `
 k ) [,) ( B `  k
) ) )  =  if ( ( A `
 k )  < 
( B `  k
) ,  ( ( B `  k )  -  ( A `  k ) ) ,  0 ) )
265 hoidmvlelem3.lt . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  W )  ->  ( A `  k )  <  ( B `  k
) )
266259, 265syldan 478 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( A `  k )  <  ( B `  k
) )
267266iftrued 3880 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  Y )  ->  if ( ( A `  k )  <  ( B `  k ) ,  ( ( B `
 k )  -  ( A `  k ) ) ,  0 )  =  ( ( B `
 k )  -  ( A `  k ) ) )
268255, 264, 2673eqtrd 2509 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  Y )  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( ( B `  k )  -  ( A `  k ) ) )
269268prodeq2dv 14054 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `
 k ) [,) ( ( B  |`  Y ) `  k
) ) )  = 
prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
) )
270269eqcomd 2477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
)  =  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) ) ) )
271270adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  Y  =/=  (/) )  ->  prod_ k  e.  Y  ( ( B `
 k )  -  ( A `  k ) )  =  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) ) ) )
272249, 250, 2713eqtr4d 2515 . . . . . . . . . . . . 13  |-  ( (
ph  /\  Y  =/=  (/) )  ->  G  =  prod_ k  e.  Y  ( ( B `  k
)  -  ( A `
 k ) ) )
273 difrp 11360 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  k
)  e.  RR  /\  ( B `  k )  e.  RR )  -> 
( ( A `  k )  <  ( B `  k )  <->  ( ( B `  k
)  -  ( A `
 k ) )  e.  RR+ ) )
274260, 262, 273syl2anc 673 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  Y )  ->  (
( A `  k
)  <  ( B `  k )  <->  ( ( B `  k )  -  ( A `  k ) )  e.  RR+ ) )
275266, 274mpbid 215 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  Y )  ->  (
( B `  k
)  -  ( A `
 k ) )  e.  RR+ )
27659, 275fprodrpcl 14087 . . . . . . . . . . . . . 14  |-  ( ph  ->  prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
)  e.  RR+ )
277276adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  Y  =/=  (/) )  ->  prod_ k  e.  Y  ( ( B `
 k )  -  ( A `  k ) )  e.  RR+ )
278272, 277eqeltrd 2549 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =/=  (/) )  ->  G  e.  RR+ )
279214adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( 1  +  E )  e.  RR+ )
280278, 279ltdivgt1 37666 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( 1  <  ( 1  +  E )  <->  ( G  /  ( 1  +  E ) )  < 
G ) )
281244, 280mpbid 215 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( G  /  ( 1  +  E ) )  < 
G )
282281adantr 472 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  ( G  / 
( 1  +  E
) )  <  G
)
283 hoidmvlelem3.i2 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  -> 
X_ k  e.  W  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
284283adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  X_ k  e.  W  ( ( A `
 k ) [,) ( B `  k
) )  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
285 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x `
 k )  e. 
_V
286285a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( x `  k
)  e.  _V )
287 hoidmvlelem3.s . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  S  e.  U )
288287elexd 3042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  S  e.  _V )
289286, 288ifcld 3915 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  e.  _V )
290289ralrimivw 2810 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. k  e.  W  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
291290adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  A. k  e.  W  if (
k  e.  Y , 
( x `  k
) ,  S )  e.  _V )
292 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )  =  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )
293292fnmpt 5714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. k  e.  W  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V  ->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) )  Fn  W
)
294291, 293syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )  Fn  W )
295 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )
296 mptexg 6151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( W  e.  Fin  ->  (
k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) )  e.  _V )
29754, 296syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) )  e. 
_V )
298297adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )  e.  _V )
299 hoidmvlelem3.o . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  O  =  ( x  e.  X_ k  e.  Y  (
( A `  k
) [,) ( B `
 k ) ) 
|->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) )
300299fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  (
k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) )  e.  _V )  ->  ( O `  x )  =  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) ) )
301295, 298, 300syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( O `  x )  =  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) ) )
302301fneq1d 5676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( ( O `  x )  Fn  W  <->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S ) )  Fn  W ) )
303294, 302mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( O `  x )  Fn  W
)
304 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k
ph
305 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k
x
306 nfixp1 7560 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )
307305, 306nfel 2624 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )
308304, 307nfan 2031 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )
309301fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( ( O `  x ) `  k )  =  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k ) )
310309adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  (
( O `  x
) `  k )  =  ( ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) ) `  k ) )
311 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  W )  ->  k  e.  W )
312289adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  W )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
313292fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  e.  W  /\  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )  ->  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S ) ) `
 k )  =  if ( k  e.  Y ,  ( x `
 k ) ,  S ) )
314311, 312, 313syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  W )  ->  (
( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k )  =  if ( k  e.  Y ,  ( x `  k ) ,  S
) )
315314adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  (
( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k )  =  if ( k  e.  Y ,  ( x `  k ) ,  S
) )
316310, 315eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  (
( O `  x
) `  k )  =  if ( k  e.  Y ,  ( x `
 k ) ,  S ) )
317 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  Y  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  ( x `
 k ) )
318317adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  k  e.  W )  /\  k  e.  Y
)  ->  if (
k  e.  Y , 
( x `  k
) ,  S )  =  ( x `  k ) )
319 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
320319elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
)  <->  ( x  Fn  Y  /\  A. k  e.  Y  ( x `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) ) )
321320simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
)  ->  A. k  e.  Y  ( x `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
322321adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  k  e.  Y )  ->  A. k  e.  Y  ( x `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
323 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  k  e.  Y )  ->  k  e.  Y )
324 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A. k  e.  Y  ( x `  k
)  e.  ( ( A `  k ) [,) ( B `  k ) )  /\  k  e.  Y )  ->  ( x `  k
)  e.  ( ( A `  k ) [,) ( B `  k ) ) )
325322, 323, 324syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  k  e.  Y )  ->  (
x `  k )  e.  ( ( A `  k ) [,) ( B `  k )
) )
326325ad4ant24 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  k  e.  W )  /\  k  e.  Y
)  ->  ( x `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
327318, 326eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  k  e.  W )  /\  k  e.  Y
)  ->  if (
k  e.  Y , 
( x `  k
) ,  S )  e.  ( ( A `
 k ) [,) ( B `  k
) ) )
328 snidg 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( Z  e.  ( X  \  Y )  ->  Z  e.  { Z } )
32948, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  Z  e.  { Z } )
330 elun2 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( Z  e.  { Z }  ->  Z  e.  ( Y  u.  { Z }
) )
331329, 330syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  Z  e.  ( Y  u.  { Z }
) )
33256a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( Y  u.  { Z } )  =  W )
333331, 332eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  Z  e.  W )
334201, 333ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( A `  Z
)  e.  RR )
335334rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( A `  Z
)  e.  RR* )
336204, 333ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( B `  Z
)  e.  RR )
337336rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( B `  Z
)  e.  RR* )
338 iccssxr 11742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( A `  Z ) [,] ( B `  Z ) )  C_  RR*
339 hoidmvlelem3.u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U  =  { z  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  |  ( G  x.  ( z  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) }
340 ssrab2 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  { z  e.  ( ( A `
 Z ) [,] ( B `  Z
) )  |  ( G  x.  ( z  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) } 
C_  ( ( A `
 Z ) [,] ( B `  Z
) )
341339, 340eqsstri 3448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U  C_  ( ( A `  Z ) [,] ( B `  Z )
)
342341, 287sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
343338, 342sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  S  e.  RR* )
344 iccgelb 11716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  S  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  ( A `  Z )  <_  S )
345335, 337, 342, 344syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( A `  Z
)  <_  S )
346 hoidmvlelem3.sb . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  S  <  ( B `
 Z ) )
347335, 337, 343, 345, 346elicod 11710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,) ( B `  Z ) ) )
348347ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  S  e.  ( ( A `  Z ) [,) ( B `  Z ) ) )
349 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  k  e.  Y  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  S )
350349adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  =  S )
35145eleq2i 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  W  <->  k  e.  ( Y  u.  { Z } ) )
352351biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  W  ->  k  e.  ( Y  u.  { Z } ) )
353352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  e.  ( Y  u.  { Z } ) )
354 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  -.  k  e.  Y )
355 elunnel1 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  ( Y  u.  { Z }
)  /\  -.  k  e.  Y )  ->  k  e.  { Z } )
356353, 354, 355syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  e.  { Z } )
357 elsni 3985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  { Z }  ->  k  =  Z )
358356, 357syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  =  Z )
359 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  Z  ->  ( A `  k )  =  ( A `  Z ) )
360 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  Z  ->  ( B `  k )  =  ( B `  Z ) )
361359, 360oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  Z  ->  (
( A `  k
) [,) ( B `
 k ) )  =  ( ( A `
 Z ) [,) ( B `  Z
) ) )
362358, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  ( ( A `  k ) [,) ( B `  k
) )  =  ( ( A `  Z
) [,) ( B `
 Z ) ) )
363362adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  ( ( A `  k ) [,) ( B `  k )
)  =  ( ( A `  Z ) [,) ( B `  Z ) ) )
364350, 363eleq12d 2543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  ( if ( k  e.  Y ,  ( x `  k ) ,  S )  e.  ( ( A `  k ) [,) ( B `  k )
)  <->  S  e.  (
( A `  Z
) [,) ( B `
 Z ) ) ) )
365348, 364mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
366365adantllr 733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  k  e.  W )  /\  -.  k  e.  Y
)  ->  if (
k  e.  Y , 
( x `  k
) ,  S )  e.  ( ( A `
 k ) [,) ( B `  k
) ) )
367327, 366pm2.61dan 808 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  ( ( A `  k ) [,) ( B `  k ) ) )
368316, 367eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  (
( O `  x
) `  k )  e.  ( ( A `  k ) [,) ( B `  k )
) )
369368ex 441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( k  e.  W  ->  ( ( O `  x ) `
 k )  e.  ( ( A `  k ) [,) ( B `  k )
) ) )
370308, 369ralrimi 2800 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
371303, 370jca 541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( ( O `  x )  Fn  W  /\  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) ) )
372 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( O `
 x )  e. 
_V
373372elixp 7547 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( O `  x )  e.  X_ k  e.  W  ( ( A `  k ) [,) ( B `  k )
)  <->  ( ( O `
 x )  Fn  W  /\  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) ) )
374371, 373sylibr 217 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( O `  x )  e.  X_ k  e.  W  (
( A `  k
) [,) ( B `
 k ) ) )
375284, 374sseldd 3419 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( O `  x )  e.  U_ j  e.  NN  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
376 eliun 4274 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  x )  e.  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  <->  E. j  e.  NN  ( O `  x )  e.  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
377375, 376sylib 201 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  E. j  e.  NN  ( O `  x )  e.  X_ k  e.  W  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
378 ixpfn 7546 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
)  ->  x  Fn  Y )
379378adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  x  Fn  Y )
380379ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  x  Fn  Y )
381 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ k  j  e.  NN
382308, 381nfan 2031 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )
383 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k
( O `  x
)
384 nfixp1 7560 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k X_ k  e.  W  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) )
385383, 384nfel 2624 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )
386382, 385nfan 2031 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
3873093adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )  /\  k  e.  Y
)  ->  ( ( O `  x ) `  k )  =  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k ) )
388289adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
389259, 388, 313syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  Y )  ->  (
( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k )  =  if ( k  e.  Y ,  ( x `  k ) ,  S
) )
3903893adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )  /\  k  e.  Y
)  ->  ( (
k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) ) `  k
)  =  if ( k  e.  Y , 
( x `  k
) ,  S ) )
3913173ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )  /\  k  e.  Y
)  ->  if (
k  e.  Y , 
( x `  k
) ,  S )  =  ( x `  k ) )
392387, 390, 3913eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )  /\  k  e.  Y
)  ->  ( x `  k )  =  ( ( O `  x
) `  k )
)
393392ad5ant125 1278 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  Y )  ->  ( x `  k
)  =  ( ( O `  x ) `
 k ) )
394 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  ( O `  x )  e.  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
395372elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( O `  x )  e.  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  <->  ( ( O `
 x )  Fn  W  /\  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) ) )
396394, 395sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  (
( O `  x
)  Fn  W  /\  A. k  e.  W  ( ( O `  x
) `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) ) )
397396simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
398258adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  k  e.  W )
399 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( A. k  e.  W  ( ( O `  x ) `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  W )  ->  (
( O `  x
) `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
400397, 398, 399syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  (
( O `  x
) `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
401400adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  Y )  ->  ( ( O `  x ) `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
402393, 401eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  /\  k  e.  Y )  ->  ( x `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
40329ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  ph )
40437ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  -> 
j  e.  NN )
405301fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( ( O `  x ) `  Z )  =  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  Z ) )
406 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) )  =  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) )
407 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  =  Z  ->  (
k  e.  Y  <->  Z  e.  Y ) )
408 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  =  Z  ->  (
x `  k )  =  ( x `  Z ) )
409407, 408ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  =  Z  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  if ( Z  e.  Y , 
( x `  Z
) ,  S ) )
410409adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  k  =  Z )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  if ( Z  e.  Y , 
( x `  Z
) ,  S ) )
411 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x `
 Z )  e. 
_V
412411a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( x `  Z
)  e.  _V )
413412, 288ifcld 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  if ( Z  e.  Y ,  ( x `
 Z ) ,  S )  e.  _V )
414406, 410, 333, 413fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S ) ) `
 Z )  =  if ( Z  e.  Y ,  ( x `
 Z ) ,  S ) )
415414adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( (
k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S
) ) `  Z
)  =  if ( Z  e.  Y , 
( x `  Z
) ,  S ) )
41648eldifbd 3403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  -.  Z  e.  Y
)
417416iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  if ( Z  e.  Y ,  ( x `
 Z ) ,  S )  =  S )
418417adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  if ( Z  e.  Y , 
( x `  Z
) ,  S )  =  S )
419405, 415, 4183eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  S  =  ( ( O `  x ) `  Z
) )
420419ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  S  =  ( ( O `  x ) `  Z ) )
421403, 333syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  Z  e.  W )
422395simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  x )  e.  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
)  ->  A. k  e.  W  ( ( O `  x ) `  k )  e.  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) ) )
423422adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  A. k  e.  W  ( ( O `  x ) `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )
424 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  Z  ->  (
( O `  x
) `  k )  =  ( ( O `
 x ) `  Z ) )
425 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  Z  ->  (
( C `  j
) `  k )  =  ( ( C `
 j ) `  Z ) )
426 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  Z  ->  (
( D `  j
) `  k )  =  ( ( D `
 j ) `  Z ) )
427425, 426oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  Z  ->  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) )  =  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) ) )
428424, 427eleq12d 2543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  Z  ->  (
( ( O `  x ) `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  <->  ( ( O `  x ) `  Z )  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ) )
429428rspcva 3134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( Z  e.  W  /\  A. k  e.  W  ( ( O `  x
) `  k )  e.  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )  ->  (
( O `  x
) `  Z )  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )
430421, 423, 429syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  -> 
( ( O `  x ) `  Z
)  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )
431420, 430eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )  /\  ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) ) )  ->  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )
4321503adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) )  ->  ( J `  j )  =  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) )
433613ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) )  ->  if ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F )  =  ( ( C `  j
)  |`  Y ) )
434432, 433eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) )  ->  ( J `  j )  =  ( ( C `  j
)  |`  Y ) )
435434fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
)