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 38429
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 10627 . . . . 5  |-  1  e.  NN
21a1i 11 . . . 4  |-  ( (
ph  /\  Y  =  (/) )  ->  1  e.  NN )
3 0le0 10706 . . . . . 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 5870 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( L `
 Y )  =  ( L `  (/) ) )
8 reseq2 5103 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( A  |`  Y )  =  ( A  |`  (/) ) )
9 res0 5112 . . . . . . . . . . 11  |-  ( A  |`  (/) )  =  (/)
109a1i 11 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( A  |`  (/) )  =  (/) )
118, 10eqtrd 2487 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( A  |`  Y )  =  (/) )
12 reseq2 5103 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( B  |`  Y )  =  ( B  |`  (/) ) )
13 res0 5112 . . . . . . . . . . 11  |-  ( B  |`  (/) )  =  (/)
1413a1i 11 . . . . . . . . . 10  |-  ( Y  =  (/)  ->  ( B  |`  (/) )  =  (/) )
1512, 14eqtrd 2487 . . . . . . . . 9  |-  ( Y  =  (/)  ->  ( B  |`  Y )  =  (/) )
167, 11, 15oveq123d 6316 . . . . . . . 8  |-  ( Y  =  (/)  ->  ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  =  ( (/) ( L `  (/) ) (/) ) )
1716adantl 468 . . . . . . 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 5769 . . . . . . . . 9  |-  (/) : (/) --> RR
2019a1i 11 . . . . . . . 8  |-  ( (
ph  /\  Y  =  (/) )  ->  (/) : (/) --> RR )
2118, 20, 20hoidmv0val 38415 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (/) ( L `
 (/) ) (/) )  =  0 )
226, 17, 213eqtrd 2491 . . . . . 6  |-  ( (
ph  /\  Y  =  (/) )  ->  G  = 
0 )
23 nfcvd 2595 . . . . . . . . . . 11  |-  ( ph  -> 
F/_ j ( P `
 1 ) )
24 nfv 1763 . . . . . . . . . . 11  |-  F/ j
ph
25 simpr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  = 
1 )  ->  j  =  1 )
2625fveq2d 5874 . . . . . . . . . . 11  |-  ( (
ph  /\  j  = 
1 )  ->  ( P `  j )  =  ( P ` 
1 ) )
27 1red 9663 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  RR )
28 rge0ssre 11747 . . . . . . . . . . . . 13  |-  ( 0 [,) +oo )  C_  RR
29 id 22 . . . . . . . . . . . . . 14  |-  ( ph  ->  ph )
301a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  NN )
311elexi 3057 . . . . . . . . . . . . . . 15  |-  1  e.  _V
32 eleq1 2519 . . . . . . . . . . . . . . . . 17  |-  ( j  =  1  ->  (
j  e.  NN  <->  1  e.  NN ) )
3332anbi2d 711 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( ph  /\  j  e.  NN )  <->  ( ph  /\  1  e.  NN ) ) )
34 fveq2 5870 . . . . . . . . . . . . . . . . 17  |-  ( j  =  1  ->  ( P `  j )  =  ( P ` 
1 ) )
3534eleq1d 2515 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( P `  j
)  e.  ( 0 [,) +oo )  <->  ( P `  1 )  e.  ( 0 [,) +oo ) ) )
3633, 35imbi12d 322 . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  NN  /\  ( ( J `  j ) ( L `
 Y ) ( K `  j ) )  e.  _V )  ->  ( P `  j
)  =  ( ( J `  j ) ( L `  Y
) ( K `  j ) ) )
4237, 39, 41syl2anc 667 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  NN  ->  ( P `  j )  =  ( ( J `
 j ) ( L `  Y ) ( K `  j
) ) )
4342adantl 468 . . . . . . . . . . . . . . . 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 3418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  Z  e.  X )
50 snssi 4119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Z  e.  X  ->  { Z }  C_  X )
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  { Z }  C_  X )
5247, 51unssd 3612 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Y  u.  { Z } )  C_  X
)
5346, 52eqsstrd 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  W  C_  X )
5444, 53ssfid 37424 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  W  e.  Fin )
55 ssun1 3599 . . . . . . . . . . . . . . . . . . . . 21  |-  Y  C_  ( Y  u.  { Z } )
5645eqcomi 2462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Y  u.  { Z }
)  =  W
5755, 56sseqtri 3466 . . . . . . . . . . . . . . . . . . . 20  |-  Y  C_  W
5857a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  C_  W )
5954, 58ssfid 37424 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Y  e.  Fin )
6059adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
Fin )
61 iftrue 3889 . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . 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 6027 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
65 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  Y  C_  W
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  Y  C_  W )
6966, 68fssresd 5755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y ) : Y --> RR )
70 reex 9635 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  e.  _V
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  RR  e.  _V )
7254, 58ssexd 4553 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  Y  e.  _V )
7372adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
_V )
7471, 73elmapd 7491 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( C `  j
)  |`  Y )  e.  ( RR  ^m  Y
)  <->  ( ( C `
 j )  |`  Y ) : Y --> RR ) )
7569, 74mpbird 236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y )  e.  ( RR  ^m  Y ) )
7675adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y )  e.  ( RR  ^m  Y
) )
7762, 76eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . 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 3892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
7978adantl 468 . . . . . . . . . . . . . . . . . . . . . 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 9649 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  Y )  ->  0  e.  RR )
81 hoidmvlelem3.f . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F  =  ( y  e.  Y  |->  0 )
8280, 81fmptd 6051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : Y --> RR )
8370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  RR  e.  _V )
8483, 59elmapd 7491 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( F  e.  ( RR  ^m  Y )  <-> 
F : Y --> RR ) )
8582, 84mpbird 236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  e.  ( RR 
^m  Y ) )
8685ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F  e.  ( RR  ^m  Y ) )
8779, 86eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . . . . . 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 6051 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  J : NN --> ( RR 
^m  Y ) )
9190ffvelrnda 6027 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  e.  ( RR  ^m  Y
) )
92 elmapi 7498 . . . . . . . . . . . . . . . . . 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 3889 . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . 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 6027 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
98 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y ) : Y --> RR )
10171, 73elmapd 7491 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( D `  j
)  |`  Y )  e.  ( RR  ^m  Y
)  <->  ( ( D `
 j )  |`  Y ) : Y --> RR ) )
102100, 101mpbird 236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y )  e.  ( RR  ^m  Y ) )
103102adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( D `  j
)  |`  Y )  e.  ( RR  ^m  Y
) )
10495, 103eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . 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 3892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
106105adantl 468 . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . . . . . 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 6051 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K : NN --> ( RR 
^m  Y ) )
111110ffvelrnda 6027 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j )  e.  ( RR  ^m  Y
) )
112 elmapi 7498 . . . . . . . . . . . . . . . . . 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 38414 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e.  ( 0 [,) +oo ) )
11543, 114eqeltrd 2531 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,) +oo ) )
11631, 36, 115vtocl 3102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( P `
 1 )  e.  ( 0 [,) +oo ) )
11729, 30, 116syl2anc 667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P `  1
)  e.  ( 0 [,) +oo ) )
11828, 117sseldi 3432 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  1
)  e.  RR )
119118recnd 9674 . . . . . . . . . . 11  |-  ( ph  ->  ( P `  1
)  e.  CC )
12023, 24, 26, 27, 119sumsnd 37357 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  {
1 }  ( P `
 j )  =  ( P `  1
) )
121120adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  Y  =  (/) )  ->  sum_ j  e. 
{ 1 }  ( P `  j )  =  ( P ` 
1 ) )
122 fveq2 5870 . . . . . . . . . . . . 13  |-  ( j  =  1  ->  ( J `  j )  =  ( J ` 
1 ) )
123 fveq2 5870 . . . . . . . . . . . . 13  |-  ( j  =  1  ->  ( K `  j )  =  ( K ` 
1 ) )
124122, 123oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  1  ->  (
( J `  j
) ( L `  Y ) ( K `
 j ) )  =  ( ( J `
 1 ) ( L `  Y ) ( K `  1
) ) )
125 ovex 6323 . . . . . . . . . . . 12  |-  ( ( J `  1 ) ( L `  Y
) ( K ` 
1 ) )  e. 
_V
126124, 40, 125fvmpt 5953 . . . . . . . . . . 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 6312 . . . . . . . . . . 11  |-  ( Y  =  (/)  ->  ( ( J `  1 ) ( L `  Y
) ( K ` 
1 ) )  =  ( ( J ` 
1 ) ( L `
 (/) ) ( K `
 1 ) ) )
130129adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  Y
) ( K ` 
1 ) )  =  ( ( J ` 
1 ) ( L `
 (/) ) ( K `
 1 ) ) )
131122feq1d 5719 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( J `  j
) : Y --> RR  <->  ( J `  1 ) : Y --> RR ) )
13233, 131imbi12d 322 . . . . . . . . . . . . . . 15  |-  ( j  =  1  ->  (
( ( ph  /\  j  e.  NN )  ->  ( J `  j
) : Y --> RR )  <-> 
( ( ph  /\  1  e.  NN )  ->  ( J `  1
) : Y --> RR ) ) )
13369adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y ) : Y --> RR )
13462feq1d 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F : Y --> RR )
13779feq1d 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR )
140 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
141 fvex 5880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( C `
 j )  e. 
_V
142141resex 5151 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C `  j )  |`  Y )  e.  _V
14362, 142syl6eqel 2539 . . . . . . . . . . . . . . . . . . 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 3058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F  e.  _V )
145144adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  NN )  ->  F  e. 
_V )
146145adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F  e.  _V )
14779, 146eqeltrd 2531 . . . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F )  e.  _V )
14989fvmpt2 5962 . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
) )
151150feq1d 5719 . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j ) : Y --> RR )
15331, 132, 152vtocl 3102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( J `
 1 ) : Y --> RR )
15429, 30, 153syl2anc 667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( J `  1
) : Y --> RR )
155154adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( J `  1 ) : Y --> RR )
156 id 22 . . . . . . . . . . . . . . 15  |-  ( Y  =  (/)  ->  Y  =  (/) )
157156eqcomd 2459 . . . . . . . . . . . . . 14  |-  ( Y  =  (/)  ->  (/)  =  Y )
158157feq2d 5720 . . . . . . . . . . . . 13  |-  ( Y  =  (/)  ->  ( ( J `  1 ) : (/) --> RR  <->  ( J `  1 ) : Y --> RR ) )
159158adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 ) : (/) --> RR  <->  ( J `  1 ) : Y --> RR ) )
160155, 159mpbird 236 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =  (/) )  ->  ( J `  1 ) :
(/) --> RR )
161123feq1d 5719 . . . . . . . . . . . . . . . 16  |-  ( j  =  1  ->  (
( K `  j
) : Y --> RR  <->  ( K `  1 ) : Y --> RR ) )
16233, 161imbi12d 322 . . . . . . . . . . . . . . 15  |-  ( j  =  1  ->  (
( ( ph  /\  j  e.  NN )  ->  ( K `  j
) : Y --> RR )  <-> 
( ( ph  /\  1  e.  NN )  ->  ( K `  1
) : Y --> RR ) ) )
16331, 162, 113vtocl 3102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  1  e.  NN )  ->  ( K `
 1 ) : Y --> RR )
16429, 30, 163syl2anc 667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( K `  1
) : Y --> RR )
165164adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( K `  1 ) : Y --> RR )
166157feq2d 5720 . . . . . . . . . . . . 13  |-  ( Y  =  (/)  ->  ( ( K `  1 ) : (/) --> RR  <->  ( K `  1 ) : Y --> RR ) )
167166adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( K `  1 ) : (/) --> RR  <->  ( K `  1 ) : Y --> RR ) )
168165, 167mpbird 236 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =  (/) )  ->  ( K `  1 ) :
(/) --> RR )
16918, 160, 168hoidmv0val 38415 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  (/) ) ( K `  1 ) )  =  0 )
170130, 169eqtrd 2487 . . . . . . . . 9  |-  ( (
ph  /\  Y  =  (/) )  ->  ( ( J `  1 )
( L `  Y
) ( K ` 
1 ) )  =  0 )
171121, 128, 1703eqtrd 2491 . . . . . . . 8  |-  ( (
ph  /\  Y  =  (/) )  ->  sum_ j  e. 
{ 1 }  ( P `  j )  =  0 )
172171oveq2d 6311 . . . . . . 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 11348 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
17527, 174readdcld 9675 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
176175recnd 9674 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  E
)  e.  CC )
177176mul01d 9837 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  0 )  =  0 )
178177adantr 467 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (
1  +  E )  x.  0 )  =  0 )
179 eqidd 2454 . . . . . . 7  |-  ( (
ph  /\  Y  =  (/) )  ->  0  = 
0 )
180172, 178, 1793eqtrd 2491 . . . . . 6  |-  ( (
ph  /\  Y  =  (/) )  ->  ( (
1  +  E )  x.  sum_ j  e.  {
1 }  ( P `
 j ) )  =  0 )
18122, 180breq12d 4418 . . . . 5  |-  ( (
ph  /\  Y  =  (/) )  ->  ( G  <_  ( ( 1  +  E )  x.  sum_ j  e.  { 1 }  ( P `  j ) )  <->  0  <_  0 ) )
1824, 181mpbird 236 . . . 4  |-  ( (
ph  /\  Y  =  (/) )  ->  G  <_  ( ( 1  +  E
)  x.  sum_ j  e.  { 1 }  ( P `  j )
) )
183 oveq2 6303 . . . . . . . . 9  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
1841nnzi 10968 . . . . . . . . . . 11  |-  1  e.  ZZ
185 fzsn 11847 . . . . . . . . . . 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 2487 . . . . . . . 8  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
189188sumeq1d 13779 . . . . . . 7  |-  ( m  =  1  ->  sum_ j  e.  ( 1 ... m
) ( P `  j )  =  sum_ j  e.  { 1 }  ( P `  j ) )
190189oveq2d 6311 . . . . . 6  |-  ( m  =  1  ->  (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... m
) ( P `  j ) )  =  ( ( 1  +  E )  x.  sum_ j  e.  { 1 }  ( P `  j ) ) )
191190breq2d 4417 . . . . 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 3152 . . . 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 667 . . 3  |-  ( (
ph  /\  Y  =  (/) )  ->  E. m  e.  NN  G  <_  (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... m
) ( P `  j ) ) )
194 simpl 459 . . . 4  |-  ( (
ph  /\  -.  Y  =  (/) )  ->  ph )
195 neqne 37384 . . . . 5  |-  ( -.  Y  =  (/)  ->  Y  =/=  (/) )
196195adantl 468 . . . 4  |-  ( (
ph  /\  -.  Y  =  (/) )  ->  Y  =/=  (/) )
197 nfv 1763 . . . . . 6  |-  F/ j ( ph  /\  Y  =/=  (/) )
198184a1i 11 . . . . . 6  |-  ( (
ph  /\  Y  =/=  (/) )  ->  1  e.  ZZ )
199 nnuz 11201 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
200115adantlr 722 . . . . . 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 5755 . . . . . . . . . . 11  |-  ( ph  ->  ( A  |`  Y ) : Y --> RR )
204 hoidmvlelem3.b . . . . . . . . . . . 12  |-  ( ph  ->  B : W --> RR )
205204, 202fssresd 5755 . . . . . . . . . . 11  |-  ( ph  ->  ( B  |`  Y ) : Y --> RR )
20618, 59, 203, 205hoidmvcl 38414 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  ( 0 [,) +oo ) )
20728, 206sseldi 3432 . . . . . . . . 9  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  RR )
2085, 207syl5eqel 2535 . . . . . . . 8  |-  ( ph  ->  G  e.  RR )
209 0red 9649 . . . . . . . . 9  |-  ( ph  ->  0  e.  RR )
210 1rp 11313 . . . . . . . . . . . . 13  |-  1  e.  RR+
211210a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  RR+ )
212211, 173jca 535 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  e.  RR+  /\  E  e.  RR+ )
)
213 rpaddcl 11330 . . . . . . . . . . 11  |-  ( ( 1  e.  RR+  /\  E  e.  RR+ )  ->  (
1  +  E )  e.  RR+ )
214212, 213syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  E
)  e.  RR+ )
215 rpgt0 11320 . . . . . . . . . 10  |-  ( ( 1  +  E )  e.  RR+  ->  0  < 
( 1  +  E
) )
216214, 215syl 17 . . . . . . . . 9  |-  ( ph  ->  0  <  ( 1  +  E ) )
217209, 216gtned 9775 . . . . . . . 8  |-  ( ph  ->  ( 1  +  E
)  =/=  0 )
218208, 175, 217redivcld 10442 . . . . . . 7  |-  ( ph  ->  ( G  /  (
1  +  E ) )  e.  RR )
219218adantr 467 . . . . . 6  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( G  /  ( 1  +  E ) )  e.  RR )
220218ltpnfd 11430 . . . . . . . . . 10  |-  ( ph  ->  ( G  /  (
1  +  E ) )  < +oo )
221220adantr 467 . . . . . . . . 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 2459 . . . . . . . . . 10  |-  ( (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo  -> +oo  =  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) ) )
224223adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  -> +oo  =  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
225221, 224breqtrd 4430 . . . . . . . 8  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( G  / 
( 1  +  E
) )  <  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
226225adantlr 722 . . . . . . 7  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( G  / 
( 1  +  E
) )  <  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) ) )
227 simpl 459 . . . . . . . 8  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( ph  /\  Y  =/=  (/) ) )
228 simpr 463 . . . . . . . . . 10  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )
229 nnex 10622 . . . . . . . . . . . 12  |-  NN  e.  _V
230229a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  NN  e.  _V )
231 icossicc 11728 . . . . . . . . . . . . . 14  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
232231, 115sseldi 3432 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,] +oo ) )
233 eqid 2453 . . . . . . . . . . . . 13  |-  ( j  e.  NN  |->  ( P `
 j ) )  =  ( j  e.  NN  |->  ( P `  j ) )
234232, 233fmptd 6051 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  e.  NN  |->  ( P `  j ) ) : NN --> ( 0 [,] +oo ) )
235234adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( j  e.  NN  |->  ( P `  j ) ) : NN --> ( 0 [,] +oo ) )
236230, 235sge0repnf 38238 . . . . . . . . . 10  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  ( (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR  <->  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo ) )
237228, 236mpbird 236 . . . . . . . . 9  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
238237adantlr 722 . . . . . . . 8  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  = +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
239219adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  ( G  / 
( 1  +  E
) )  e.  RR )
240208adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  G  e.  RR )
241240adantlr 722 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  G  e.  RR )
242 simpr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  =/=  (/) )  /\  (Σ^ `  (
j  e.  NN  |->  ( P `  j ) ) )  e.  RR )  ->  (Σ^ `  ( j  e.  NN  |->  ( P `  j ) ) )  e.  RR )
24327, 173ltaddrpd 11378 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  ( 1  +  E ) )
244243adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =/=  (/) )  ->  1  <  ( 1  +  E ) )
24559adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  Y  e.  Fin )
246 simpr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  Y  =/=  (/) )
247203adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( A  |`  Y ) : Y --> RR )
248205adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( B  |`  Y ) : Y --> RR )
24918, 245, 246, 247, 248hoidmvn0val 38416 . . . . . . . . . . . . . 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 5884 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  (
( A  |`  Y ) `
 k )  =  ( A `  k
) )
252 fvres 5884 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  (
( B  |`  Y ) `
 k )  =  ( B `  k
) )
253251, 252oveq12d 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  Y  ->  (
( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) )  =  ( ( A `  k ) [,) ( B `  k )
) )
254253fveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  Y  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( vol `  ( ( A `  k ) [,) ( B `  k )
) ) )
255254adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  Y )  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( vol `  ( ( A `  k ) [,) ( B `  k )
) ) )
256201adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  A : W --> RR )
257 elun1 3603 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  Y  ->  k  e.  ( Y  u.  { Z } ) )
258257, 45syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Y  ->  k  e.  W )
259258adantl 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  k  e.  W )
260256, 259ffvelrnd 6028 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( A `  k )  e.  RR )
261204adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  Y )  ->  B : W --> RR )
262261, 259ffvelrnd 6028 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( B `  k )  e.  RR )
263 volico 38373 . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  Y )  ->  ( A `  k )  <  ( B `  k
) )
267266iftrued 3891 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  Y )  ->  if ( ( A `  k )  <  ( B `  k ) ,  ( ( B `
 k )  -  ( A `  k ) ) ,  0 )  =  ( ( B `
 k )  -  ( A `  k ) ) )
268255, 264, 2673eqtrd 2491 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  Y )  ->  ( vol `  ( ( ( A  |`  Y ) `  k ) [,) (
( B  |`  Y ) `
 k ) ) )  =  ( ( B `  k )  -  ( A `  k ) ) )
269268prodeq2dv 13989 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `
 k ) [,) ( ( B  |`  Y ) `  k
) ) )  = 
prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
) )
270269eqcomd 2459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
)  =  prod_ k  e.  Y  ( vol `  ( ( ( A  |`  Y ) `  k
) [,) ( ( B  |`  Y ) `  k ) ) ) )
271270adantr 467 . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . 13  |-  ( (
ph  /\  Y  =/=  (/) )  ->  G  =  prod_ k  e.  Y  ( ( B `  k
)  -  ( A `
 k ) ) )
273 difrp 11344 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  k
)  e.  RR  /\  ( B `  k )  e.  RR )  -> 
( ( A `  k )  <  ( B `  k )  <->  ( ( B `  k
)  -  ( A `
 k ) )  e.  RR+ ) )
274260, 262, 273syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  Y )  ->  (
( A `  k
)  <  ( B `  k )  <->  ( ( B `  k )  -  ( A `  k ) )  e.  RR+ ) )
275266, 274mpbid 214 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  Y )  ->  (
( B `  k
)  -  ( A `
 k ) )  e.  RR+ )
27659, 275fprodrpcl 14022 . . . . . . . . . . . . . 14  |-  ( ph  ->  prod_ k  e.  Y  ( ( B `  k )  -  ( A `  k )
)  e.  RR+ )
277276adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  Y  =/=  (/) )  ->  prod_ k  e.  Y  ( ( B `
 k )  -  ( A `  k ) )  e.  RR+ )
278272, 277eqeltrd 2531 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =/=  (/) )  ->  G  e.  RR+ )
279214adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( 1  +  E )  e.  RR+ )
280278, 279ltdivgt1 37589 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( 1  <  ( 1  +  E )  <->  ( G  /  ( 1  +  E ) )  < 
G ) )
281244, 280mpbid 214 . . . . . . . . . 10  |-  ( (
ph  /\  Y  =/=  (/) )  ->  ( G  /  ( 1  +  E ) )  < 
G )
282281adantr 467 . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . 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 5880 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x `
 k )  e. 
_V
286285a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( x `  k
)  e.  _V )
287 hoidmvlelem3.s . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  S  e.  U )
288287elexd 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  S  e.  _V )
289286, 288ifcld 3926 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  e.  _V )
290289ralrimivw 2805 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. k  e.  W  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
291290adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 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 2453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )  =  ( k  e.  W  |->  if ( k  e.  Y , 
( x `  k
) ,  S ) )
293292fnmpt 5709 . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )
296 mptexg 6140 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . 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 5671 . . . . . . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  ( O `  x )  Fn  W
)
304 nfv 1763 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k
ph
305 nfcv 2594 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k
x
306 nfixp1 7547 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )
307305, 306nfel 2606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )
308304, 307nfan 2013 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )
309301fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  W )  ->  k  e.  W )
312289adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  W )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
313292fvmpt2 5962 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  W )  ->  (
( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k )  =  if ( k  e.  Y ,  ( x `  k ) ,  S
) )
315314adantlr 722 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . . . . . . . . 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 3889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  Y  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  ( x `
 k ) )
318317adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
320319elixp 7534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
)  ->  A. k  e.  Y  ( x `  k )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
322321adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  k  e.  Y )  ->  k  e.  Y )
324 rspa 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k
) )  /\  k  e.  Y )  ->  (
x `  k )  e.  ( ( A `  k ) [,) ( B `  k )
) )
326325ad4ant24 1241 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( Z  e.  ( X  \  Y )  ->  Z  e.  { Z } )
32948, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  Z  e.  { Z } )
330 elun2 3604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  Z  e.  W )
334201, 333ffvelrnd 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( A `  Z
)  e.  RR )
335334rexrd 9695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( A `  Z
)  e.  RR* )
336204, 333ffvelrnd 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( B `  Z
)  e.  RR )
337336rexrd 9695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( B `  Z
)  e.  RR* )
338 iccssxr 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U  C_  ( ( A `  Z ) [,] ( B `  Z )
)
342341, 287sseldi 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
343338, 342sseldi 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  S  e.  RR* )
344 iccgelb 11698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  S  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  ( A `  Z )  <_  S )
345335, 337, 342, 344syl3anc 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( A `  Z
)  <_  S )
346 hoidmvlelem3.sb . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  S  <  ( B `
 Z ) )
347335, 337, 343, 345, 346elicod 11692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,) ( B `  Z ) ) )
348347ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  S  e.  ( ( A `  Z ) [,) ( B `  Z ) ) )
349 iffalse 3892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  k  e.  Y  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  S )
350349adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  =  S )
35145eleq2i 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  W  <->  k  e.  ( Y  u.  { Z } ) )
352351biimpi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  W  ->  k  e.  ( Y  u.  { Z } ) )
353352adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  e.  ( Y  u.  { Z } ) )
354 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  -.  k  e.  Y )
355 elunnel1 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  ( Y  u.  { Z }
)  /\  -.  k  e.  Y )  ->  k  e.  { Z } )
356353, 354, 355syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  e.  { Z } )
357 elsni 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  { Z }  ->  k  =  Z )
358356, 357syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  W  /\  -.  k  e.  Y
)  ->  k  =  Z )
359 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  Z  ->  ( A `  k )  =  ( A `  Z ) )
360 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  Z  ->  ( B `  k )  =  ( B `  Z ) )
361359, 360oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  ( ( A `  k ) [,) ( B `  k )
)  =  ( ( A `  Z ) [,) ( B `  Z ) ) )
364350, 363eleq12d 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  W )  /\  -.  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `
 k ) ,  S )  e.  ( ( A `  k
) [,) ( B `
 k ) ) )
366365adantllr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
) )  /\  k  e.  W )  ->  (
( O `  x
) `  k )  e.  ( ( A `  k ) [,) ( B `  k )
) )
369368ex 436 . . . . . . . . . . . . . . . . . . . . . . 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 2790 . . . . . . . . . . . . . . . . . . . . . 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 535 . . . . . . . . . . . . . . . . . . . . 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 5880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( O `
 x )  e. 
_V
373372elixp 7534 . . . . . . . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . . . . . . . . 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 3435 . . . . . . . . . . . . . . . . . . 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 4286 . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . 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 7533 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  X_ k  e.  Y  ( ( A `  k ) [,) ( B `  k )
)  ->  x  Fn  Y )
379378adantl 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  x  Fn  Y )
380379ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . 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 1763 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ k  j  e.  NN
382308, 381nfan 2013 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k ( ( ph  /\  x  e.  X_ k  e.  Y  ( ( A `
 k ) [,) ( B `  k
) ) )  /\  j  e.  NN )
383 nfcv 2594 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k
( O `  x
)
384 nfixp1 7547 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k X_ k  e.  W  ( ( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) )
385383, 384nfel 2606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )
386382, 385nfan 2013 . . . . . . . . . . . . . . . . . . . . . . 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 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  Y )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  e.  _V )
389259, 388, 313syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  Y )  ->  (
( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) `  k )  =  if ( k  e.  Y ,  ( x `  k ) ,  S
) )
3903893adant2 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) )  /\  k  e.  Y
)  ->  ( x `  k )  =  ( ( O `  x
) `  k )
)
393392ad5ant125 1255 . . . . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( O `  x
)  e.  X_ k  e.  W  ( (
( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  /\  k  e.  Y )  ->  k  e.  W )
399 rspa 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) )  =  ( k  e.  W  |->  if ( k  e.  Y ,  ( x `
 k ) ,  S ) ) )
407 eleq1 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  =  Z  ->  (
k  e.  Y  <->  Z  e.  Y ) )
408 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  =  Z  ->  (
x `  k )  =  ( x `  Z ) )
409407, 408ifbieq1d 3906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  =  Z  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  if ( Z  e.  Y , 
( x `  Z
) ,  S ) )
410409adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  k  =  Z )  ->  if ( k  e.  Y ,  ( x `  k ) ,  S
)  =  if ( Z  e.  Y , 
( x `  Z
) ,  S ) )
411 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x `
 Z )  e. 
_V
412411a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( x `  Z
)  e.  _V )
413412, 288ifcld 3926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  if ( Z  e.  Y ,  ( x `
 Z ) ,  S )  e.  _V )
414406, 410, 333, 413fvmptd 5959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( ( k  e.  W  |->  if ( k  e.  Y ,  ( x `  k ) ,  S ) ) `
 Z )  =  if ( Z  e.  Y ,  ( x `
 Z ) ,  S ) )
415414adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  -.  Z  e.  Y
)
417416iffalsed 3894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  if ( Z  e.  Y ,  ( x `
 Z ) ,  S )  =  S )
418417adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  if ( Z  e.  Y , 
( x `  Z
) ,  S )  =  S )
419405, 415, 4183eqtrrd 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  X_ k  e.  Y  ( ( A `  k
) [,) ( B `
 k ) ) )  ->  S  =  ( ( O `  x ) `  Z
) )
420419ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  Z  ->  (
( O `  x
) `  k )  =  ( ( O `
 x ) `  Z ) )
425 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  Z  ->  (
( C `  j
) `  k )  =  ( ( C `
 j ) `  Z ) )
426 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  Z  ->  (
( D `  j
) `  k )  =  ( ( D `
 j ) `  Z ) )
427425, 426oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  Z  ->  (
( ( C `  j ) `  k
) [,) ( ( D `  j ) `
 k ) )  =  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) ) )
428424, 427eleq12d 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  Z  ->  (
( ( O `  x ) `  k
)  e.  ( ( ( C `  j
) `  k ) [,) ( ( D `  j ) `  k
) )  <->  ( ( O `  x ) `  Z )  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ) )
429428rspcva 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) )  ->  ( J `  j )  =  ( ( C `  j
)  |`  Y ) )
435434fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  NN  /\  S  e.  ( ( ( C `  j ) `  Z
)