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

Theorem hoidmvle 38540
Description: The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvle.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 )
) ) ) ) )
hoidmvle.x  |-  ( ph  ->  X  e.  Fin )
hoidmvle.a  |-  ( ph  ->  A : X --> RR )
hoidmvle.b  |-  ( ph  ->  B : X --> RR )
hoidmvle.c  |-  ( ph  ->  C : NN --> ( RR 
^m  X ) )
hoidmvle.d  |-  ( ph  ->  D : NN --> ( RR 
^m  X ) )
hoidmvle.s  |-  ( ph  -> 
X_ k  e.  X  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
Assertion
Ref Expression
hoidmvle  |-  ( ph  ->  ( A ( L `
 X ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 X ) ( D `  j ) ) ) ) )
Distinct variable groups:    A, a,
b, k    B, b,
k    C, j, k    D, j, k    L, a, b, j, x    X, a, b, j, k, x    ph, a, b, j, x
Allowed substitution hints:    ph( k)    A( x, j)    B( x, j, a)    C( x, a, b)    D( x, a, b)    L( k)

Proof of Theorem hoidmvle
Dummy variables  c 
d  e  f  g  h  i  l  o  u  v  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmvle.s . 2  |-  ( ph  -> 
X_ k  e.  X  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
2 hoidmvle.d . . . 4  |-  ( ph  ->  D : NN --> ( RR 
^m  X ) )
3 ovex 6336 . . . . . . 7  |-  ( RR 
^m  X )  e. 
_V
4 nnex 10637 . . . . . . 7  |-  NN  e.  _V
53, 4pm3.2i 462 . . . . . 6  |-  ( ( RR  ^m  X )  e.  _V  /\  NN  e.  _V )
65a1i 11 . . . . 5  |-  ( ph  ->  ( ( RR  ^m  X )  e.  _V  /\  NN  e.  _V )
)
7 elmapg 7503 . . . . 5  |-  ( ( ( RR  ^m  X
)  e.  _V  /\  NN  e.  _V )  -> 
( D  e.  ( ( RR  ^m  X
)  ^m  NN )  <->  D : NN --> ( RR 
^m  X ) ) )
86, 7syl 17 . . . 4  |-  ( ph  ->  ( D  e.  ( ( RR  ^m  X
)  ^m  NN )  <->  D : NN --> ( RR 
^m  X ) ) )
92, 8mpbird 240 . . 3  |-  ( ph  ->  D  e.  ( ( RR  ^m  X )  ^m  NN ) )
10 hoidmvle.c . . . . 5  |-  ( ph  ->  C : NN --> ( RR 
^m  X ) )
11 elmapg 7503 . . . . . 6  |-  ( ( ( RR  ^m  X
)  e.  _V  /\  NN  e.  _V )  -> 
( C  e.  ( ( RR  ^m  X
)  ^m  NN )  <->  C : NN --> ( RR 
^m  X ) ) )
126, 11syl 17 . . . . 5  |-  ( ph  ->  ( C  e.  ( ( RR  ^m  X
)  ^m  NN )  <->  C : NN --> ( RR 
^m  X ) ) )
1310, 12mpbird 240 . . . 4  |-  ( ph  ->  C  e.  ( ( RR  ^m  X )  ^m  NN ) )
14 hoidmvle.b . . . . . 6  |-  ( ph  ->  B : X --> RR )
15 reex 9648 . . . . . . . . 9  |-  RR  e.  _V
1615a1i 11 . . . . . . . 8  |-  ( ph  ->  RR  e.  _V )
17 hoidmvle.x . . . . . . . 8  |-  ( ph  ->  X  e.  Fin )
1816, 17jca 541 . . . . . . 7  |-  ( ph  ->  ( RR  e.  _V  /\  X  e.  Fin )
)
19 elmapg 7503 . . . . . . 7  |-  ( ( RR  e.  _V  /\  X  e.  Fin )  ->  ( B  e.  ( RR  ^m  X )  <-> 
B : X --> RR ) )
2018, 19syl 17 . . . . . 6  |-  ( ph  ->  ( B  e.  ( RR  ^m  X )  <-> 
B : X --> RR ) )
2114, 20mpbird 240 . . . . 5  |-  ( ph  ->  B  e.  ( RR 
^m  X ) )
22 hoidmvle.a . . . . . . 7  |-  ( ph  ->  A : X --> RR )
23 elmapg 7503 . . . . . . . 8  |-  ( ( RR  e.  _V  /\  X  e.  Fin )  ->  ( A  e.  ( RR  ^m  X )  <-> 
A : X --> RR ) )
2418, 23syl 17 . . . . . . 7  |-  ( ph  ->  ( A  e.  ( RR  ^m  X )  <-> 
A : X --> RR ) )
2522, 24mpbird 240 . . . . . 6  |-  ( ph  ->  A  e.  ( RR 
^m  X ) )
26 oveq2 6316 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( RR 
^m  x )  =  ( RR  ^m  (/) ) )
2726eleq2d 2534 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( a  e.  ( RR  ^m  x )  <->  a  e.  ( RR  ^m  (/) ) ) )
2826eleq2d 2534 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( b  e.  ( RR  ^m  x )  <->  b  e.  ( RR  ^m  (/) ) ) )
2926oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( x  =  (/)  ->  ( ( RR  ^m  x )  ^m  NN )  =  ( ( RR  ^m  (/) )  ^m  NN ) )
3029eleq2d 2534 . . . . . . . . . . . . 13  |-  ( x  =  (/)  ->  ( c  e.  ( ( RR 
^m  x )  ^m  NN )  <->  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) ) )
3129eleq2d 2534 . . . . . . . . . . . . . . 15  |-  ( x  =  (/)  ->  ( d  e.  ( ( RR 
^m  x )  ^m  NN )  <->  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ) )
32 ixpeq1 7551 . . . . . . . . . . . . . . . . 17  |-  ( x  =  (/)  ->  X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  =  X_ k  e.  (/)  ( ( a `  k ) [,) ( b `  k ) ) )
33 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  (/)  ->  X_ k  e.  x  ( (
( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  =  X_ k  e.  (/)  ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) ) )
3433iuneq2d 4296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  (/)  ->  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  =  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) )
3532, 34sseq12d 3447 . . . . . . . . . . . . . . . 16  |-  ( x  =  (/)  ->  ( X_ k  e.  x  (
( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  <->  X_ k  e.  (/)  ( ( a `  k ) [,) ( b `  k ) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) ) ) )
36 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  (/)  ->  ( L `
 x )  =  ( L `  (/) ) )
3736oveqd 6325 . . . . . . . . . . . . . . . . 17  |-  ( x  =  (/)  ->  ( a ( L `  x
) b )  =  ( a ( L `
 (/) ) b ) )
3836oveqd 6325 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  (/)  ->  ( ( c `  j ) ( L `  x
) ( d `  j ) )  =  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) )
3938mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  (/)  ->  ( j  e.  NN  |->  ( ( c `  j ) ( L `  x
) ( d `  j ) ) )  =  ( j  e.  NN  |->  ( ( c `
 j ) ( L `  (/) ) ( d `  j ) ) ) )
4039fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  (/)  ->  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  =  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) )
4137, 40breq12d 4408 . . . . . . . . . . . . . . . 16  |-  ( x  =  (/)  ->  ( ( a ( L `  x ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  <->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
4235, 41imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( x  =  (/)  ->  ( (
X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <-> 
( X_ k  e.  (/)  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) )
4331, 42imbi12d 327 . . . . . . . . . . . . . 14  |-  ( x  =  (/)  ->  ( ( d  e.  ( ( RR  ^m  x )  ^m  NN )  -> 
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  ->  ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) ) )
4443ralbidv2 2827 . . . . . . . . . . . . 13  |-  ( x  =  (/)  ->  ( A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) )
4530, 44imbi12d 327 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  ( ( c  e.  ( ( RR  ^m  x )  ^m  NN )  ->  A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) ) )
4645ralbidv2 2827 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. c  e.  (
( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) )
4728, 46imbi12d 327 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( b  e.  ( RR 
^m  x )  ->  A. c  e.  (
( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( b  e.  ( RR  ^m  (/) )  ->  A. c  e.  (
( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) ) )
4847ralbidv2 2827 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. b  e.  ( RR  ^m  (/) ) A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) )
4927, 48imbi12d 327 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( a  e.  ( RR 
^m  x )  ->  A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( a  e.  ( RR  ^m  (/) )  ->  A. b  e.  ( RR  ^m  (/) ) A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) ) )
5049ralbidv2 2827 . . . . . . 7  |-  ( x  =  (/)  ->  ( A. a  e.  ( RR  ^m  x ) A. b  e.  ( RR  ^m  x
) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. a  e.  ( RR  ^m  (/) ) A. b  e.  ( RR  ^m  (/) ) A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) ) )
51 oveq2 6316 . . . . . . . . . 10  |-  ( x  =  y  ->  ( RR  ^m  x )  =  ( RR  ^m  y
) )
5251eleq2d 2534 . . . . . . . . 9  |-  ( x  =  y  ->  (
a  e.  ( RR 
^m  x )  <->  a  e.  ( RR  ^m  y
) ) )
5351eleq2d 2534 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
b  e.  ( RR 
^m  x )  <->  b  e.  ( RR  ^m  y
) ) )
5451oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
( RR  ^m  x
)  ^m  NN )  =  ( ( RR 
^m  y )  ^m  NN ) )
5554eleq2d 2534 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
c  e.  ( ( RR  ^m  x )  ^m  NN )  <->  c  e.  ( ( RR  ^m  y )  ^m  NN ) ) )
5654eleq2d 2534 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
d  e.  ( ( RR  ^m  x )  ^m  NN )  <->  d  e.  ( ( RR  ^m  y )  ^m  NN ) ) )
57 ixpeq1 7551 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  =  X_ k  e.  y  (
( a `  k
) [,) ( b `
 k ) ) )
58 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  X_ k  e.  x  ( (
( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  =  X_ k  e.  y  (
( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) ) )
5958iuneq2d 4296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  =  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) )
6057, 59sseq12d 3447 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( X_ k  e.  x  ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  <->  X_ k  e.  y 
( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) ) )
61 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( L `  x )  =  ( L `  y ) )
6261oveqd 6325 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
a ( L `  x ) b )  =  ( a ( L `  y ) b ) )
6361oveqd 6325 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( c `  j
) ( L `  x ) ( d `
 j ) )  =  ( ( c `
 j ) ( L `  y ) ( d `  j
) ) )
6463mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) )  =  ( j  e.  NN  |->  ( ( c `  j ) ( L `  y
) ( d `  j ) ) ) )
6564fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  y ) ( d `
 j ) ) ) ) )
6662, 65breq12d 4408 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( a ( L `
 x ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  <->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) )
6760, 66imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <-> 
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
6856, 67imbi12d 327 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
( d  e.  ( ( RR  ^m  x
)  ^m  NN )  ->  ( X_ k  e.  x  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( d  e.  ( ( RR  ^m  y )  ^m  NN )  ->  ( X_ k  e.  y  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) ) )
6968ralbidv2 2827 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
7055, 69imbi12d 327 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( c  e.  ( ( RR  ^m  x
)  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( c  e.  ( ( RR  ^m  y )  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) ) )
7170ralbidv2 2827 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( A. c  e.  (
( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. c  e.  (
( RR  ^m  y
)  ^m  NN ) A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
7253, 71imbi12d 327 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( b  e.  ( RR  ^m  x )  ->  A. c  e.  ( ( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( b  e.  ( RR  ^m  y
)  ->  A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) ) )
7372ralbidv2 2827 . . . . . . . . 9  |-  ( x  =  y  ->  ( A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. b  e.  ( RR  ^m  y ) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y )  ^m  NN ) ( X_ k  e.  y  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
7452, 73imbi12d 327 . . . . . . . 8  |-  ( x  =  y  ->  (
( a  e.  ( RR  ^m  x )  ->  A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( a  e.  ( RR  ^m  y
)  ->  A. b  e.  ( RR  ^m  y
) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) ) )
7574ralbidv2 2827 . . . . . . 7  |-  ( x  =  y  ->  ( A. a  e.  ( RR  ^m  x ) A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. a  e.  ( RR  ^m  y ) A. b  e.  ( RR  ^m  y ) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
76 oveq2 6316 . . . . . . . . . 10  |-  ( x  =  ( y  u. 
{ z } )  ->  ( RR  ^m  x )  =  ( RR  ^m  ( y  u.  { z } ) ) )
7776eleq2d 2534 . . . . . . . . 9  |-  ( x  =  ( y  u. 
{ z } )  ->  ( a  e.  ( RR  ^m  x
)  <->  a  e.  ( RR  ^m  ( y  u.  { z } ) ) ) )
7876eleq2d 2534 . . . . . . . . . . 11  |-  ( x  =  ( y  u. 
{ z } )  ->  ( b  e.  ( RR  ^m  x
)  <->  b  e.  ( RR  ^m  ( y  u.  { z } ) ) ) )
7976oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( RR 
^m  x )  ^m  NN )  =  (
( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) )
8079eleq2d 2534 . . . . . . . . . . . . 13  |-  ( x  =  ( y  u. 
{ z } )  ->  ( c  e.  ( ( RR  ^m  x )  ^m  NN ) 
<->  c  e.  ( ( RR  ^m  ( y  u.  { z } ) )  ^m  NN ) ) )
8179eleq2d 2534 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  u. 
{ z } )  ->  ( d  e.  ( ( RR  ^m  x )  ^m  NN ) 
<->  d  e.  ( ( RR  ^m  ( y  u.  { z } ) )  ^m  NN ) ) )
82 ixpeq1 7551 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  u. 
{ z } )  ->  X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  =  X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) )
83 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( y  u. 
{ z } )  ->  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  =  X_ k  e.  ( y  u.  {
z } ) ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) ) )
8483iuneq2d 4296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  u. 
{ z } )  ->  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  =  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) ) )
8582, 84sseq12d 3447 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  u. 
{ z } )  ->  ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  <->  X_ k  e.  ( y  u.  { z } ) ( ( a `  k ) [,) ( b `  k ) )  C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) ) )
86 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( y  u. 
{ z } )  ->  ( L `  x )  =  ( L `  ( y  u.  { z } ) ) )
8786oveqd 6325 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  u. 
{ z } )  ->  ( a ( L `  x ) b )  =  ( a ( L `  ( y  u.  {
z } ) ) b ) )
8886oveqd 6325 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( c `
 j ) ( L `  x ) ( d `  j
) )  =  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) )
8988mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( y  u. 
{ z } )  ->  ( j  e.  NN  |->  ( ( c `
 j ) ( L `  x ) ( d `  j
) ) )  =  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 ( y  u. 
{ z } ) ) ( d `  j ) ) ) )
9089fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  u. 
{ z } )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  =  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 ( y  u. 
{ z } ) ) ( d `  j ) ) ) ) )
9187, 90breq12d 4408 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( a ( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  <->  ( a
( L `  (
y  u.  { z } ) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 ( y  u. 
{ z } ) ) ( d `  j ) ) ) ) ) )
9285, 91imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( X_ k  e.  x  (
( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  ->  ( a ( L `  x ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) ) ) )  <->  ( X_ k  e.  ( y  u.  { z } ) ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) )
9381, 92imbi12d 327 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( d  e.  ( ( RR 
^m  x )  ^m  NN )  ->  ( X_ k  e.  x  (
( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  ->  ( a ( L `  x ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) ) ) ) )  <-> 
( d  e.  ( ( RR  ^m  (
y  u.  { z } ) )  ^m  NN )  ->  ( X_ k  e.  ( y  u.  { z } ) ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) ) )
9493ralbidv2 2827 . . . . . . . . . . . . 13  |-  ( x  =  ( y  u. 
{ z } )  ->  ( A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) ( X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j ) `
 k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) )
9580, 94imbi12d 327 . . . . . . . . . . . 12  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( c  e.  ( ( RR 
^m  x )  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( c  e.  ( ( RR  ^m  ( y  u.  {
z } ) )  ^m  NN )  ->  A. d  e.  (
( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) ( X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j ) `
 k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) ) )
9695ralbidv2 2827 . . . . . . . . . . 11  |-  ( x  =  ( y  u. 
{ z } )  ->  ( A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. c  e.  (
( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) A. d  e.  ( ( RR  ^m  ( y  u.  {
z } ) )  ^m  NN ) (
X_ k  e.  ( y  u.  { z } ) ( ( a `  k ) [,) ( b `  k ) )  C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (
y  u.  { z } ) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 ( y  u. 
{ z } ) ) ( d `  j ) ) ) ) ) ) )
9778, 96imbi12d 327 . . . . . . . . . 10  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( b  e.  ( RR  ^m  x )  ->  A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( b  e.  ( RR  ^m  (
y  u.  { z } ) )  ->  A. c  e.  (
( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) A. d  e.  ( ( RR  ^m  ( y  u.  {
z } ) )  ^m  NN ) (
X_ k  e.  ( y  u.  { z } ) ( ( a `  k ) [,) ( b `  k ) )  C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (
y  u.  { z } ) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 ( y  u. 
{ z } ) ) ( d `  j ) ) ) ) ) ) ) )
9897ralbidv2 2827 . . . . . . . . 9  |-  ( x  =  ( y  u. 
{ z } )  ->  ( A. b  e.  ( RR  ^m  x
) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. b  e.  ( RR  ^m  ( y  u. 
{ z } ) ) A. c  e.  ( ( RR  ^m  ( y  u.  {
z } ) )  ^m  NN ) A. d  e.  ( ( RR  ^m  ( y  u. 
{ z } ) )  ^m  NN ) ( X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j ) `
 k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) )
9977, 98imbi12d 327 . . . . . . . 8  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( a  e.  ( RR  ^m  x )  ->  A. b  e.  ( RR  ^m  x
) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( a  e.  ( RR  ^m  (
y  u.  { z } ) )  ->  A. b  e.  ( RR  ^m  ( y  u. 
{ z } ) ) A. c  e.  ( ( RR  ^m  ( y  u.  {
z } ) )  ^m  NN ) A. d  e.  ( ( RR  ^m  ( y  u. 
{ z } ) )  ^m  NN ) ( X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j ) `
 k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) ) )
10099ralbidv2 2827 . . . . . . 7  |-  ( x  =  ( y  u. 
{ z } )  ->  ( A. a  e.  ( RR  ^m  x
) A. b  e.  ( RR  ^m  x
) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. a  e.  ( RR  ^m  ( y  u. 
{ z } ) ) A. b  e.  ( RR  ^m  (
y  u.  { z } ) ) A. c  e.  ( ( RR  ^m  ( y  u. 
{ z } ) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (
y  u.  { z } ) )  ^m  NN ) ( X_ k  e.  ( y  u.  {
z } ) ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  ( y  u.  { z } ) ( ( ( c `  j ) `
 k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  ( y  u.  {
z } ) ) b )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  ( y  u.  {
z } ) ) ( d `  j
) ) ) ) ) ) )
101 oveq2 6316 . . . . . . . . . 10  |-  ( x  =  X  ->  ( RR  ^m  x )  =  ( RR  ^m  X
) )
102101eleq2d 2534 . . . . . . . . 9  |-  ( x  =  X  ->  (
a  e.  ( RR 
^m  x )  <->  a  e.  ( RR  ^m  X ) ) )
103101eleq2d 2534 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
b  e.  ( RR 
^m  x )  <->  b  e.  ( RR  ^m  X ) ) )
104101oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( RR  ^m  x
)  ^m  NN )  =  ( ( RR 
^m  X )  ^m  NN ) )
105104eleq2d 2534 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
c  e.  ( ( RR  ^m  x )  ^m  NN )  <->  c  e.  ( ( RR  ^m  X )  ^m  NN ) ) )
106104eleq2d 2534 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
d  e.  ( ( RR  ^m  x )  ^m  NN )  <->  d  e.  ( ( RR  ^m  X )  ^m  NN ) ) )
107 ixpeq1 7551 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  =  X_ k  e.  X  (
( a `  k
) [,) ( b `
 k ) ) )
108 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  X_ k  e.  x  ( (
( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  =  X_ k  e.  X  (
( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) ) )
109108iuneq2d 4296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  =  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) )
110107, 109sseq12d 3447 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( X_ k  e.  x  ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  <->  X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) ) )
111 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  ( L `  x )  =  ( L `  X ) )
112111oveqd 6325 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
a ( L `  x ) b )  =  ( a ( L `  X ) b ) )
113111oveqd 6325 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  (
( c `  j
) ( L `  x ) ( d `
 j ) )  =  ( ( c `
 j ) ( L `  X ) ( d `  j
) ) )
114113mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) )  =  ( j  e.  NN  |->  ( ( c `  j ) ( L `  X
) ( d `  j ) ) ) )
115114fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  x ) ( d `
 j ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  X ) ( d `
 j ) ) ) ) )
116112, 115breq12d 4408 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( a ( L `
 x ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) )  <->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) )
117110, 116imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <-> 
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) )
118106, 117imbi12d 327 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( d  e.  ( ( RR  ^m  x
)  ^m  NN )  ->  ( X_ k  e.  x  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( d  e.  ( ( RR  ^m  X )  ^m  NN )  ->  ( X_ k  e.  X  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) ) )
119118ralbidv2 2827 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) )
120105, 119imbi12d 327 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( c  e.  ( ( RR  ^m  x
)  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( c  e.  ( ( RR  ^m  X )  ^m  NN )  ->  A. d  e.  ( ( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) ) )
121120ralbidv2 2827 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( A. c  e.  (
( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. c  e.  (
( RR  ^m  X
)  ^m  NN ) A. d  e.  (
( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) )
122103, 121imbi12d 327 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( b  e.  ( RR  ^m  x )  ->  A. c  e.  ( ( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( b  e.  ( RR  ^m  X
)  ->  A. c  e.  ( ( RR  ^m  X )  ^m  NN ) A. d  e.  ( ( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) ) )
123122ralbidv2 2827 . . . . . . . . 9  |-  ( x  =  X  ->  ( A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x )  ^m  NN ) ( X_ k  e.  x  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. b  e.  ( RR  ^m  X ) A. c  e.  ( ( RR  ^m  X )  ^m  NN ) A. d  e.  ( ( RR  ^m  X )  ^m  NN ) ( X_ k  e.  X  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) )
124102, 123imbi12d 327 . . . . . . . 8  |-  ( x  =  X  ->  (
( a  e.  ( RR  ^m  x )  ->  A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x
)  ^m  NN ) A. d  e.  (
( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) ) )  <->  ( a  e.  ( RR  ^m  X
)  ->  A. b  e.  ( RR  ^m  X
) A. c  e.  ( ( RR  ^m  X )  ^m  NN ) A. d  e.  ( ( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) ) )
125124ralbidv2 2827 . . . . . . 7  |-  ( x  =  X  ->  ( A. a  e.  ( RR  ^m  x ) A. b  e.  ( RR  ^m  x ) A. c  e.  ( ( RR  ^m  x )  ^m  NN ) A. d  e.  ( ( RR  ^m  x
)  ^m  NN )
( X_ k  e.  x  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  x  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  x
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 x ) ( d `  j ) ) ) ) )  <->  A. a  e.  ( RR  ^m  X ) A. b  e.  ( RR  ^m  X ) A. c  e.  ( ( RR  ^m  X )  ^m  NN ) A. d  e.  ( ( RR  ^m  X
)  ^m  NN )
( X_ k  e.  X  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  X
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 X ) ( d `  j ) ) ) ) ) ) )
126 hoidmvle.l . . . . . . . . . . . . . . . 16  |-  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 )
) ) ) ) )
127 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  e  ->  (
a `  k )  =  ( e `  k ) )
128127oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  e  ->  (
( a `  k
) [,) ( b `
 k ) )  =  ( ( e `
 k ) [,) ( b `  k
) ) )
129128fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  e  ->  ( vol `  ( ( a `
 k ) [,) ( b `  k
) ) )  =  ( vol `  (
( e `  k
) [,) ( b `
 k ) ) ) )
130129prodeq2ad 37769 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  e  ->  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) )  =  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
b `  k )
) ) )
131130ifeq2d 3891 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  e  ->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) ( b `  k ) ) ) )  =  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) ( b `  k ) ) ) ) )
132 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  f  ->  (
b `  k )  =  ( f `  k ) )
133132oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  f  ->  (
( e `  k
) [,) ( b `
 k ) )  =  ( ( e `
 k ) [,) ( f `  k
) ) )
134133fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  f  ->  ( vol `  ( ( e `
 k ) [,) ( b `  k
) ) )  =  ( vol `  (
( e `  k
) [,) ( f `
 k ) ) ) )
135134prodeq2ad 37769 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  f  ->  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
b `  k )
) )  =  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
f `  k )
) ) )
136135ifeq2d 3891 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  f  ->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) ( b `  k ) ) ) )  =  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) ( f `  k ) ) ) ) )
137131, 136cbvmpt2v 6390 . . . . . . . . . . . . . . . . 17  |-  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x )  |->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) ( b `  k ) ) ) ) )  =  ( e  e.  ( RR 
^m  x ) ,  f  e.  ( RR 
^m  x )  |->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
f `  k )
) ) ) )
138137mpteq2i 4479 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) ) ) )  =  ( x  e.  Fin  |->  ( e  e.  ( RR  ^m  x ) ,  f  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
f `  k )
) ) ) ) )
139126, 138eqtri 2493 . . . . . . . . . . . . . . 15  |-  L  =  ( x  e.  Fin  |->  ( e  e.  ( RR  ^m  x ) ,  f  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( e `  k ) [,) (
f `  k )
) ) ) ) )
140 elmapi 7511 . . . . . . . . . . . . . . . 16  |-  ( a  e.  ( RR  ^m  (/) )  ->  a : (/) --> RR )
141140adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  ( RR 
^m  (/) )  /\  b  e.  ( RR  ^m  (/) ) )  ->  a : (/) --> RR )
142 elmapi 7511 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( RR  ^m  (/) )  ->  b : (/) --> RR )
143142adantl 473 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  ( RR 
^m  (/) )  /\  b  e.  ( RR  ^m  (/) ) )  ->  b : (/) --> RR )
144139, 141, 143hoidmv0val 38523 . . . . . . . . . . . . . 14  |-  ( ( a  e.  ( RR 
^m  (/) )  /\  b  e.  ( RR  ^m  (/) ) )  ->  ( a ( L `  (/) ) b )  =  0 )
145144ad5ant23 1270 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  a  e.  ( RR 
^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  /\  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  ( a
( L `  (/) ) b )  =  0 )
146 nfv 1769 . . . . . . . . . . . . . . 15  |-  F/ j ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )
1474a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  NN  e.  _V )
148 icossicc 11746 . . . . . . . . . . . . . . . 16  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
149 0fin 7817 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  Fin
150149a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  j  e.  NN )  ->  (/)  e.  Fin )
151 ovex 6336 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
^m  (/) )  e.  _V
152151a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  ( RR  ^m  (/) )  e.  _V )
1534a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  NN  e.  _V )
154 simpl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )
155 simpr 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  j  e.  NN )
156152, 153, 154, 155fvmap 37546 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  (
c `  j )  e.  ( RR  ^m  (/) ) )
157 elmapi 7511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c `  j )  e.  ( RR  ^m  (/) )  ->  ( c `  j ) : (/) --> RR )
158156, 157syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  (
c `  j ) : (/) --> RR )
159158adantlr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  j  e.  NN )  ->  (
c `  j ) : (/) --> RR )
160151a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  ( RR  ^m  (/) )  e.  _V )
1614a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  NN  e.  _V )
162 simpl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )
163 simpr 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  j  e.  NN )
164160, 161, 162, 163fvmap 37546 . . . . . . . . . . . . . . . . . . 19  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  (
d `  j )  e.  ( RR  ^m  (/) ) )
165 elmapi 7511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( d `  j )  e.  ( RR  ^m  (/) )  ->  ( d `  j ) : (/) --> RR )
166164, 165syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( d  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  j  e.  NN )  ->  (
d `  j ) : (/) --> RR )
167166adantll 728 . . . . . . . . . . . . . . . . 17  |-  ( ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  j  e.  NN )  ->  (
d `  j ) : (/) --> RR )
168126, 150, 159, 167hoidmvcl 38522 . . . . . . . . . . . . . . . 16  |-  ( ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  j  e.  NN )  ->  (
( c `  j
) ( L `  (/) ) ( d `  j ) )  e.  ( 0 [,) +oo ) )
169148, 168sseldi 3416 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  j  e.  NN )  ->  (
( c `  j
) ( L `  (/) ) ( d `  j ) )  e.  ( 0 [,] +oo ) )
170146, 147, 169sge0ge0mpt 38394 . . . . . . . . . . . . . 14  |-  ( ( c  e.  ( ( RR  ^m  (/) )  ^m  NN )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  0  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  (/) ) ( d `  j ) ) ) ) )
171170adantll 728 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  a  e.  ( RR 
^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  /\  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  0  <_  (Σ^ `  (
j  e.  NN  |->  ( ( c `  j
) ( L `  (/) ) ( d `  j ) ) ) ) )
172145, 171eqbrtrd 4416 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  a  e.  ( RR 
^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  /\  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) )
173172a1d 25 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  a  e.  ( RR 
^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  /\  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  /\  d  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  ( X_ k  e.  (/)  ( ( a `  k ) [,) ( b `  k ) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `  j
) `  k ) [,) ( ( d `  j ) `  k
) )  ->  (
a ( L `  (/) ) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
174173ralrimiva 2809 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  ( RR  ^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  /\  c  e.  ( ( RR  ^m  (/) )  ^m  NN ) )  ->  A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
175174ralrimiva 2809 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  ( RR  ^m  (/) ) )  /\  b  e.  ( RR  ^m  (/) ) )  ->  A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
176175ralrimiva 2809 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( RR  ^m  (/) ) )  ->  A. b  e.  ( RR  ^m  (/) ) A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
177176ralrimiva 2809 . . . . . . 7  |-  ( ph  ->  A. a  e.  ( RR  ^m  (/) ) A. b  e.  ( RR  ^m  (/) ) A. c  e.  ( ( RR  ^m  (/) )  ^m  NN ) A. d  e.  ( ( RR  ^m  (/) )  ^m  NN ) ( X_ k  e.  (/)  ( ( a `
 k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  (/)  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  (/) ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 (/) ) ( d `
 j ) ) ) ) ) )
178 simpl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  C_  X  /\  z  e.  ( X  \  y ) ) )  /\  A. a  e.  ( RR  ^m  y
) A. b  e.  ( RR  ^m  y
) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) )  ->  ( ph  /\  ( y  C_  X  /\  z  e.  ( X  \  y ) ) ) )
179128ixpeq2dv 7556 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  e  ->  X_ k  e.  y  ( (
a `  k ) [,) ( b `  k
) )  =  X_ k  e.  y  (
( e `  k
) [,) ( b `
 k ) ) )
180179sseq1d 3445 . . . . . . . . . . . . . . . . 17  |-  ( a  =  e  ->  ( X_ k  e.  y  ( ( a `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  <->  X_ k  e.  y 
( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) ) )
181 oveq1 6315 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  e  ->  (
a ( L `  y ) b )  =  ( e ( L `  y ) b ) )
182181breq1d 4405 . . . . . . . . . . . . . . . . 17  |-  ( a  =  e  ->  (
( a ( L `
 y ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) )  <->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) )
183180, 182imbi12d 327 . . . . . . . . . . . . . . . 16  |-  ( a  =  e  ->  (
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <-> 
( X_ k  e.  y  ( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
184183ralbidv 2829 . . . . . . . . . . . . . . 15  |-  ( a  =  e  ->  ( A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
185184ralbidv 2829 . . . . . . . . . . . . . 14  |-  ( a  =  e  ->  ( A. c  e.  (
( RR  ^m  y
)  ^m  NN ) A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( a `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <->  A. c  e.  (
( RR  ^m  y
)  ^m  NN ) A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
186185ralbidv 2829 . . . . . . . . . . . . 13  |-  ( a  =  e  ->  ( A. b  e.  ( RR  ^m  y ) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y )  ^m  NN ) ( X_ k  e.  y  ( (
a `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( a
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <->  A. b  e.  ( RR  ^m  y ) A. c  e.  ( ( RR  ^m  y )  ^m  NN ) A. d  e.  ( ( RR  ^m  y )  ^m  NN ) ( X_ k  e.  y  ( (
e `  k ) [,) ( b `  k
) )  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
187133ixpeq2dv 7556 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  f  ->  X_ k  e.  y  ( (
e `  k ) [,) ( b `  k
) )  =  X_ k  e.  y  (
( e `  k
) [,) ( f `
 k ) ) )
188187sseq1d 3445 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  f  ->  ( X_ k  e.  y  ( ( e `  k
) [,) ( b `
 k ) ) 
C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `  j ) `  k
) [,) ( ( d `  j ) `
 k ) )  <->  X_ k  e.  y 
( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
) ) )
189 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  f  ->  (
e ( L `  y ) b )  =  ( e ( L `  y ) f ) )
190189breq1d 4405 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  f  ->  (
( e ( L `
 y ) b )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) )  <->  ( e
( L `  y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) )
191188, 190imbi12d 327 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  f  ->  (
( X_ k  e.  y  ( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <-> 
( X_ k  e.  y  ( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) ) ) )
192191ralbidv 2829 . . . . . . . . . . . . . . . . 17  |-  ( b  =  f  ->  ( A. d  e.  (
( RR  ^m  y
)  ^m  NN )
( X_ k  e.  y  ( ( e `  k ) [,) (
b `  k )
)  C_  U_ j  e.  NN  X_ k  e.  y  ( ( ( c `
 j ) `  k ) [,) (
( d `  j
) `  k )
)  ->  ( e
( L `  y
) b )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( c `  j ) ( L `
 y ) ( d `  j ) ) ) ) )  <->  A. d  e.  (
( RR  ^m  y
)  ^m