Metamath Proof Explorer

Theorem ovnlecvr2

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ovnlecvr2.x 
|- ( ph -> X e. Fin )
ovnlecvr2.c 
|- ( ph -> C : NN --> ( RR ^m X ) )
ovnlecvr2.d 
|- ( ph -> D : NN --> ( RR ^m X ) )
ovnlecvr2.s 
|- ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
ovnlecvr2.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 ) ) ) ) ) )
Assertion ovnlecvr2 
|- ( ph -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnlecvr2.x 
 |-  ( ph -> X e. Fin )
2 ovnlecvr2.c 
 |-  ( ph -> C : NN --> ( RR ^m X ) )
3 ovnlecvr2.d 
 |-  ( ph -> D : NN --> ( RR ^m X ) )
4 ovnlecvr2.s 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
5 ovnlecvr2.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 ) ) ) ) ) )
6 fveq2 
 |-  ( X = (/) -> ( voln* ` X ) = ( voln* ` (/) ) )
7 6 fveq1d 
 |-  ( X = (/) -> ( ( voln* ` X ) ` A ) = ( ( voln* ` (/) ) ` A ) )
8 7 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) = ( ( voln* ` (/) ) ` A ) )
9 4 adantr 
 |-  ( ( ph /\ X = (/) ) -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
10 1nn 
 |-  1 e. NN
11 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
12 10 11 ax-mp 
 |-  NN =/= (/)
13 12 a1i 
 |-  ( ph -> NN =/= (/) )
14 iunconst 
 |-  ( NN =/= (/) -> U_ j e. NN { (/) } = { (/) } )
15 13 14 syl 
 |-  ( ph -> U_ j e. NN { (/) } = { (/) } )
16 15 adantr 
 |-  ( ( ph /\ X = (/) ) -> U_ j e. NN { (/) } = { (/) } )
17 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. (/) ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
18 ixp0x 
 |-  X_ k e. (/) ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = { (/) }
19 18 a1i 
 |-  ( X = (/) -> X_ k e. (/) ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = { (/) } )
20 17 19 eqtrd 
 |-  ( X = (/) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = { (/) } )
21 20 adantr 
 |-  ( ( X = (/) /\ j e. NN ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = { (/) } )
22 21 iuneq2dv 
 |-  ( X = (/) -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = U_ j e. NN { (/) } )
23 22 adantl 
 |-  ( ( ph /\ X = (/) ) -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = U_ j e. NN { (/) } )
24 reex 
 |-  RR e. _V
25 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
26 24 25 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
27 26 a1i 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m (/) ) = { (/) } )
28 16 23 27 3eqtr4d 
 |-  ( ( ph /\ X = (/) ) -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( RR ^m (/) ) )
29 9 28 sseqtrd 
 |-  ( ( ph /\ X = (/) ) -> A C_ ( RR ^m (/) ) )
30 29 ovn0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` (/) ) ` A ) = 0 )
31 8 30 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) = 0 )
32 nfv 
 |-  F/ j ph
33 nnex 
 |-  NN e. _V
34 33 a1i 
 |-  ( ph -> NN e. _V )
35 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
36 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
37 2 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m X ) )
38 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m X ) -> ( C ` j ) : X --> RR )
39 37 38 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : X --> RR )
40 3 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m X ) )
41 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m X ) -> ( D ` j ) : X --> RR )
42 40 41 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : X --> RR )
43 5 36 39 42 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) e. ( 0 [,) +oo ) )
44 35 43 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) e. ( 0 [,] +oo ) )
45 32 34 44 sge0ge0mpt 
 |-  ( ph -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
46 45 adantr 
 |-  ( ( ph /\ X = (/) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
47 31 46 eqbrtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
48 simpl 
 |-  ( ( ph /\ -. X = (/) ) -> ph )
49 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
50 49 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
51 1 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
52 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
53 39 ffvelrnda 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR )
54 42 ffvelrnda 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR )
55 54 rexrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR* )
56 icossre 
 |-  ( ( ( ( C ` j ) ` k ) e. RR /\ ( ( D ` j ) ` k ) e. RR* ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
57 53 55 56 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
58 57 ralrimiva 
 |-  ( ( ph /\ j e. NN ) -> A. k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
59 ss2ixp 
 |-  ( A. k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ X_ k e. X RR )
60 58 59 syl 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ X_ k e. X RR )
61 24 a1i 
 |-  ( ph -> RR e. _V )
62 ixpconstg 
 |-  ( ( X e. Fin /\ RR e. _V ) -> X_ k e. X RR = ( RR ^m X ) )
63 1 61 62 syl2anc 
 |-  ( ph -> X_ k e. X RR = ( RR ^m X ) )
64 63 adantr 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X RR = ( RR ^m X ) )
65 60 64 sseqtrd 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ ( RR ^m X ) )
66 65 ralrimiva 
 |-  ( ph -> A. j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ ( RR ^m X ) )
67 iunss 
 |-  ( U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ ( RR ^m X ) <-> A. j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ ( RR ^m X ) )
68 66 67 sylibr 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ ( RR ^m X ) )
69 4 68 sstrd 
 |-  ( ph -> A C_ ( RR ^m X ) )
70 69 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> A C_ ( RR ^m X ) )
71 eqid 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
72 51 52 70 71 ovnn0val 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln* ` X ) ` A ) = inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) )
73 ssrab2 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR*
74 73 a1i 
 |-  ( ( ph /\ X =/= (/) ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR* )
75 32 34 44 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. RR* )
76 75 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. RR* )
77 opelxpi 
 |-  ( ( ( ( C ` j ) ` k ) e. RR /\ ( ( D ` j ) ` k ) e. RR ) -> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. e. ( RR X. RR ) )
78 53 54 77 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. e. ( RR X. RR ) )
79 78 fmpttd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) : X --> ( RR X. RR ) )
80 24 24 xpex 
 |-  ( RR X. RR ) e. _V
81 80 a1i 
 |-  ( ( ph /\ j e. NN ) -> ( RR X. RR ) e. _V )
82 elmapg 
 |-  ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) : X --> ( RR X. RR ) ) )
83 81 36 82 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) : X --> ( RR X. RR ) ) )
84 79 83 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. ( ( RR X. RR ) ^m X ) )
85 84 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) : NN --> ( ( RR X. RR ) ^m X ) )
86 ovexd 
 |-  ( ph -> ( ( RR X. RR ) ^m X ) e. _V )
87 elmapg 
 |-  ( ( ( ( RR X. RR ) ^m X ) e. _V /\ NN e. _V ) -> ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) : NN --> ( ( RR X. RR ) ^m X ) ) )
88 86 34 87 syl2anc 
 |-  ( ph -> ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) : NN --> ( ( RR X. RR ) ^m X ) ) )
89 85 88 mpbird 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
90 89 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
91 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
92 mptexg 
 |-  ( X e. Fin -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. _V )
93 1 92 syl 
 |-  ( ph -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. _V )
94 93 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. _V )
95 eqid 
 |-  ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
96 95 fvmpt2 
 |-  ( ( j e. NN /\ ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) e. _V ) -> ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) = ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
97 91 94 96 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) = ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
98 97 coeq2d 
 |-  ( ( ph /\ j e. NN ) -> ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) = ( [,) o. ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) )
99 98 fveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) = ( ( [,) o. ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` k ) )
100 99 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) = ( ( [,) o. ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` k ) )
101 79 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) : X --> ( RR X. RR ) )
102 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> k e. X )
103 101 102 fvovco 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` k ) = ( ( 1st ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) [,) ( 2nd ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) ) )
104 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
105 opex 
 |-  <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. e. _V
106 105 a1i 
 |-  ( ( ph /\ k e. X ) -> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. e. _V )
107 eqid 
 |-  ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. )
108 107 fvmpt2 
 |-  ( ( k e. X /\ <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. e. _V ) -> ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) = <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. )
109 104 106 108 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) = <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. )
110 109 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) = ( 1st ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
111 fvex 
 |-  ( ( C ` j ) ` k ) e. _V
112 fvex 
 |-  ( ( D ` j ) ` k ) e. _V
113 op1stg 
 |-  ( ( ( ( C ` j ) ` k ) e. _V /\ ( ( D ` j ) ` k ) e. _V ) -> ( 1st ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( ( C ` j ) ` k ) )
114 111 112 113 mp2an 
 |-  ( 1st ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( ( C ` j ) ` k )
115 114 a1i 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( ( C ` j ) ` k ) )
116 110 115 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) = ( ( C ` j ) ` k ) )
117 109 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) = ( 2nd ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
118 111 112 op2nd 
 |-  ( 2nd ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( ( D ` j ) ` k )
119 118 a1i 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) = ( ( D ` j ) ` k ) )
120 117 119 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) = ( ( D ` j ) ` k ) )
121 116 120 oveq12d 
 |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) [,) ( 2nd ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
122 121 adantlr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) [,) ( 2nd ` ( ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ` k ) ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
123 100 103 122 3eqtrrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
124 123 ixpeq2dva 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
125 124 iuneq2dv 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
126 4 125 sseqtrd 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
127 126 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
128 eqidd 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) )
129 51 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. NN ) -> X e. Fin )
130 52 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. NN ) -> X =/= (/) )
131 39 adantlr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. NN ) -> ( C ` j ) : X --> RR )
132 42 adantlr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. NN ) -> ( D ` j ) : X --> RR )
133 5 129 130 131 132 hoidmvn0val 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) = prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
134 133 mpteq2dva 
 |-  ( ( ph /\ X =/= (/) ) -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) )
135 134 fveq2d 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) )
136 123 eqcomd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
137 136 fveq2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) = ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
138 137 prodeq2dv 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
139 138 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) )
140 139 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) )
141 140 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) )
142 128 135 141 3eqtr4d 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) )
143 127 142 jca 
 |-  ( ( ph /\ X =/= (/) ) -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) ) )
144 nfcv 
 |-  F/_ j i
145 nfmpt1 
 |-  F/_ j ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
146 144 145 nfeq 
 |-  F/ j i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
147 nfcv 
 |-  F/_ k i
148 nfcv 
 |-  F/_ k NN
149 nfmpt1 
 |-  F/_ k ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. )
150 148 149 nfmpt 
 |-  F/_ k ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
151 147 150 nfeq 
 |-  F/ k i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) )
152 fveq1 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( i ` j ) = ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) )
153 152 coeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( [,) o. ( i ` j ) ) = ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) )
154 153 fveq1d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
155 154 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ k e. X ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
156 151 155 ixpeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
157 156 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
158 146 157 iuneq2df 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) )
159 158 sseq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) )
160 nfv 
 |-  F/ k j e. NN
161 151 160 nfan 
 |-  F/ k ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ j e. NN )
162 154 fveq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) )
163 162 a1d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( k e. X -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) )
164 163 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ j e. NN ) -> ( k e. X -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) )
165 161 164 ralrimi 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ j e. NN ) -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) )
166 165 prodeq2d 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) )
167 146 166 mpteq2da 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) )
168 167 fveq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) )
169 168 eqeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) ) )
170 159 169 anbi12d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) -> ( ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) ) ) )
171 170 rspcev 
 |-  ( ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. ( ( C ` j ) ` k ) , ( ( D ` j ) ` k ) >. ) ) ` j ) ) ` k ) ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
172 90 143 171 syl2anc 
 |-  ( ( ph /\ X =/= (/) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
173 76 172 jca 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
174 eqeq1 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
175 174 anbi2d 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) -> ( ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
176 175 rexbidv 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
177 176 elrab 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } <-> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
178 173 177 sylibr 
 |-  ( ( ph /\ X =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
179 infxrlb 
 |-  ( ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR* /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } ) -> inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
180 74 178 179 syl2anc 
 |-  ( ( ph /\ X =/= (/) ) -> inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
181 72 180 eqbrtrd 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
182 48 50 181 syl2anc 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
183 47 182 pm2.61dan 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )