Metamath Proof Explorer

Theorem ovnovollem1

Description: if F is a cover of B in RR , then I is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnovollem1.a 
|- ( ph -> A e. V )
ovnovollem1.f 
|- ( ph -> F e. ( ( RR X. RR ) ^m NN ) )
ovnovollem1.i 
|- I = ( j e. NN |-> { <. A , ( F ` j ) >. } )
ovnovollem1.s 
|- ( ph -> B C_ U. ran ( [,) o. F ) )
ovnovollem1.b 
|- ( ph -> B e. W )
ovnovollem1.z 
|- ( ph -> Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
Assertion ovnovollem1 
|- ( ph -> E. i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnovollem1.a 
 |-  ( ph -> A e. V )
2 ovnovollem1.f 
 |-  ( ph -> F e. ( ( RR X. RR ) ^m NN ) )
3 ovnovollem1.i 
 |-  I = ( j e. NN |-> { <. A , ( F ` j ) >. } )
4 ovnovollem1.s 
 |-  ( ph -> B C_ U. ran ( [,) o. F ) )
5 ovnovollem1.b 
 |-  ( ph -> B e. W )
6 ovnovollem1.z 
 |-  ( ph -> Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
7 eqidd 
 |-  ( ( ph /\ j e. NN ) -> { <. A , ( F ` j ) >. } = { <. A , ( F ` j ) >. } )
8 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> A e. V )
9 elmapi 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) -> F : NN --> ( RR X. RR ) )
10 2 9 syl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
11 10 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR X. RR ) )
12 fsng 
 |-  ( ( A e. V /\ ( F ` j ) e. ( RR X. RR ) ) -> ( { <. A , ( F ` j ) >. } : { A } --> { ( F ` j ) } <-> { <. A , ( F ` j ) >. } = { <. A , ( F ` j ) >. } ) )
13 8 11 12 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( { <. A , ( F ` j ) >. } : { A } --> { ( F ` j ) } <-> { <. A , ( F ` j ) >. } = { <. A , ( F ` j ) >. } ) )
14 7 13 mpbird 
 |-  ( ( ph /\ j e. NN ) -> { <. A , ( F ` j ) >. } : { A } --> { ( F ` j ) } )
15 11 snssd 
 |-  ( ( ph /\ j e. NN ) -> { ( F ` j ) } C_ ( RR X. RR ) )
16 14 15 fssd 
 |-  ( ( ph /\ j e. NN ) -> { <. A , ( F ` j ) >. } : { A } --> ( RR X. RR ) )
17 reex 
 |-  RR e. _V
18 17 17 xpex 
 |-  ( RR X. RR ) e. _V
19 18 a1i 
 |-  ( ( ph /\ j e. NN ) -> ( RR X. RR ) e. _V )
20 snex 
 |-  { A } e. _V
21 20 a1i 
 |-  ( ( ph /\ j e. NN ) -> { A } e. _V )
22 19 21 elmapd 
 |-  ( ( ph /\ j e. NN ) -> ( { <. A , ( F ` j ) >. } e. ( ( RR X. RR ) ^m { A } ) <-> { <. A , ( F ` j ) >. } : { A } --> ( RR X. RR ) ) )
23 16 22 mpbird 
 |-  ( ( ph /\ j e. NN ) -> { <. A , ( F ` j ) >. } e. ( ( RR X. RR ) ^m { A } ) )
24 23 3 fmptd 
 |-  ( ph -> I : NN --> ( ( RR X. RR ) ^m { A } ) )
25 ovexd 
 |-  ( ph -> ( ( RR X. RR ) ^m { A } ) e. _V )
26 nnex 
 |-  NN e. _V
27 26 a1i 
 |-  ( ph -> NN e. _V )
28 25 27 elmapd 
 |-  ( ph -> ( I e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m { A } ) ) )
29 24 28 mpbird 
 |-  ( ph -> I e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) )
30 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
31 30 a1i 
 |-  ( ph -> [,) : ( RR* X. RR* ) --> ~P RR* )
32 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
33 32 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR* X. RR* ) )
34 31 33 10 fcoss 
 |-  ( ph -> ( [,) o. F ) : NN --> ~P RR* )
35 34 ffnd 
 |-  ( ph -> ( [,) o. F ) Fn NN )
36 fniunfv 
 |-  ( ( [,) o. F ) Fn NN -> U_ j e. NN ( ( [,) o. F ) ` j ) = U. ran ( [,) o. F ) )
37 35 36 syl 
 |-  ( ph -> U_ j e. NN ( ( [,) o. F ) ` j ) = U. ran ( [,) o. F ) )
38 37 eqcomd 
 |-  ( ph -> U. ran ( [,) o. F ) = U_ j e. NN ( ( [,) o. F ) ` j ) )
39 4 38 sseqtrd 
 |-  ( ph -> B C_ U_ j e. NN ( ( [,) o. F ) ` j ) )
40 fvex 
 |-  ( ( [,) o. F ) ` j ) e. _V
41 26 40 iunex 
 |-  U_ j e. NN ( ( [,) o. F ) ` j ) e. _V
42 41 a1i 
 |-  ( ph -> U_ j e. NN ( ( [,) o. F ) ` j ) e. _V )
43 20 a1i 
 |-  ( ph -> { A } e. _V )
44 1 snn0d 
 |-  ( ph -> { A } =/= (/) )
45 5 42 43 44 mapss2 
 |-  ( ph -> ( B C_ U_ j e. NN ( ( [,) o. F ) ` j ) <-> ( B ^m { A } ) C_ ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) ) )
46 39 45 mpbid 
 |-  ( ph -> ( B ^m { A } ) C_ ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) )
47 nfv 
 |-  F/ j ph
48 fvexd 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( F ` j ) ) e. _V )
49 47 27 48 1 iunmapsn 
 |-  ( ph -> U_ j e. NN ( ( [,) ` ( F ` j ) ) ^m { A } ) = ( U_ j e. NN ( [,) ` ( F ` j ) ) ^m { A } ) )
50 49 eqcomd 
 |-  ( ph -> ( U_ j e. NN ( [,) ` ( F ` j ) ) ^m { A } ) = U_ j e. NN ( ( [,) ` ( F ` j ) ) ^m { A } ) )
51 elmapfun 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) -> Fun F )
52 2 51 syl 
 |-  ( ph -> Fun F )
53 52 adantr 
 |-  ( ( ph /\ j e. NN ) -> Fun F )
54 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
55 10 fdmd 
 |-  ( ph -> dom F = NN )
56 55 eqcomd 
 |-  ( ph -> NN = dom F )
57 56 adantr 
 |-  ( ( ph /\ j e. NN ) -> NN = dom F )
58 54 57 eleqtrd 
 |-  ( ( ph /\ j e. NN ) -> j e. dom F )
59 fvco 
 |-  ( ( Fun F /\ j e. dom F ) -> ( ( [,) o. F ) ` j ) = ( [,) ` ( F ` j ) ) )
60 53 58 59 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. F ) ` j ) = ( [,) ` ( F ` j ) ) )
61 60 iuneq2dv 
 |-  ( ph -> U_ j e. NN ( ( [,) o. F ) ` j ) = U_ j e. NN ( [,) ` ( F ` j ) ) )
62 61 oveq1d 
 |-  ( ph -> ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) = ( U_ j e. NN ( [,) ` ( F ` j ) ) ^m { A } ) )
63 14 ffund 
 |-  ( ( ph /\ j e. NN ) -> Fun { <. A , ( F ` j ) >. } )
64 id 
 |-  ( j e. NN -> j e. NN )
65 snex 
 |-  { <. A , ( F ` j ) >. } e. _V
66 65 a1i 
 |-  ( j e. NN -> { <. A , ( F ` j ) >. } e. _V )
67 3 fvmpt2 
 |-  ( ( j e. NN /\ { <. A , ( F ` j ) >. } e. _V ) -> ( I ` j ) = { <. A , ( F ` j ) >. } )
68 64 66 67 syl2anc 
 |-  ( j e. NN -> ( I ` j ) = { <. A , ( F ` j ) >. } )
69 68 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) = { <. A , ( F ` j ) >. } )
70 69 funeqd 
 |-  ( ( ph /\ j e. NN ) -> ( Fun ( I ` j ) <-> Fun { <. A , ( F ` j ) >. } ) )
71 63 70 mpbird 
 |-  ( ( ph /\ j e. NN ) -> Fun ( I ` j ) )
72 71 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> Fun ( I ` j ) )
73 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> k e. { A } )
74 69 dmeqd 
 |-  ( ( ph /\ j e. NN ) -> dom ( I ` j ) = dom { <. A , ( F ` j ) >. } )
75 14 fdmd 
 |-  ( ( ph /\ j e. NN ) -> dom { <. A , ( F ` j ) >. } = { A } )
76 74 75 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> dom ( I ` j ) = { A } )
77 76 eleq2d 
 |-  ( ( ph /\ j e. NN ) -> ( k e. dom ( I ` j ) <-> k e. { A } ) )
78 77 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( k e. dom ( I ` j ) <-> k e. { A } ) )
79 73 78 mpbird 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> k e. dom ( I ` j ) )
80 fvco 
 |-  ( ( Fun ( I ` j ) /\ k e. dom ( I ` j ) ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( [,) ` ( ( I ` j ) ` k ) ) )
81 72 79 80 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( [,) ` ( ( I ` j ) ` k ) ) )
82 68 fveq1d 
 |-  ( j e. NN -> ( ( I ` j ) ` k ) = ( { <. A , ( F ` j ) >. } ` k ) )
83 82 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( I ` j ) ` k ) = ( { <. A , ( F ` j ) >. } ` k ) )
84 elsni 
 |-  ( k e. { A } -> k = A )
85 84 fveq2d 
 |-  ( k e. { A } -> ( { <. A , ( F ` j ) >. } ` k ) = ( { <. A , ( F ` j ) >. } ` A ) )
86 85 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( { <. A , ( F ` j ) >. } ` k ) = ( { <. A , ( F ` j ) >. } ` A ) )
87 fvexd 
 |-  ( ph -> ( F ` j ) e. _V )
88 fvsng 
 |-  ( ( A e. V /\ ( F ` j ) e. _V ) -> ( { <. A , ( F ` j ) >. } ` A ) = ( F ` j ) )
89 1 87 88 syl2anc 
 |-  ( ph -> ( { <. A , ( F ` j ) >. } ` A ) = ( F ` j ) )
90 89 ad2antrr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( { <. A , ( F ` j ) >. } ` A ) = ( F ` j ) )
91 83 86 90 3eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( I ` j ) ` k ) = ( F ` j ) )
92 91 fveq2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( [,) ` ( ( I ` j ) ` k ) ) = ( [,) ` ( F ` j ) ) )
93 eqidd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( [,) ` ( F ` j ) ) = ( [,) ` ( F ` j ) ) )
94 81 92 93 3eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( [,) ` ( F ` j ) ) )
95 94 ixpeq2dva 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = X_ k e. { A } ( [,) ` ( F ` j ) ) )
96 fvex 
 |-  ( [,) ` ( F ` j ) ) e. _V
97 20 96 ixpconst 
 |-  X_ k e. { A } ( [,) ` ( F ` j ) ) = ( ( [,) ` ( F ` j ) ) ^m { A } )
98 97 a1i 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( [,) ` ( F ` j ) ) = ( ( [,) ` ( F ` j ) ) ^m { A } ) )
99 95 98 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = ( ( [,) ` ( F ` j ) ) ^m { A } ) )
100 99 iuneq2dv 
 |-  ( ph -> U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = U_ j e. NN ( ( [,) ` ( F ` j ) ) ^m { A } ) )
101 50 62 100 3eqtr4d 
 |-  ( ph -> ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) = U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) )
102 46 101 sseqtrd 
 |-  ( ph -> ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) )
103 nfcv 
 |-  F/_ j F
104 ressxr 
 |-  RR C_ RR*
105 xpss2 
 |-  ( RR C_ RR* -> ( RR X. RR ) C_ ( RR X. RR* ) )
106 104 105 ax-mp 
 |-  ( RR X. RR ) C_ ( RR X. RR* )
107 106 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR X. RR* ) )
108 10 107 fssd 
 |-  ( ph -> F : NN --> ( RR X. RR* ) )
109 103 108 volicofmpt 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( j e. NN |-> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) ) )
110 68 coeq2d 
 |-  ( j e. NN -> ( [,) o. ( I ` j ) ) = ( [,) o. { <. A , ( F ` j ) >. } ) )
111 110 fveq1d 
 |-  ( j e. NN -> ( ( [,) o. ( I ` j ) ) ` A ) = ( ( [,) o. { <. A , ( F ` j ) >. } ) ` A ) )
112 111 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( ( [,) o. { <. A , ( F ` j ) >. } ) ` A ) )
113 snidg 
 |-  ( A e. V -> A e. { A } )
114 1 113 syl 
 |-  ( ph -> A e. { A } )
115 dmsnopg 
 |-  ( ( F ` j ) e. _V -> dom { <. A , ( F ` j ) >. } = { A } )
116 87 115 syl 
 |-  ( ph -> dom { <. A , ( F ` j ) >. } = { A } )
117 114 116 eleqtrrd 
 |-  ( ph -> A e. dom { <. A , ( F ` j ) >. } )
118 117 adantr 
 |-  ( ( ph /\ j e. NN ) -> A e. dom { <. A , ( F ` j ) >. } )
119 fvco 
 |-  ( ( Fun { <. A , ( F ` j ) >. } /\ A e. dom { <. A , ( F ` j ) >. } ) -> ( ( [,) o. { <. A , ( F ` j ) >. } ) ` A ) = ( [,) ` ( { <. A , ( F ` j ) >. } ` A ) ) )
120 63 118 119 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. { <. A , ( F ` j ) >. } ) ` A ) = ( [,) ` ( { <. A , ( F ` j ) >. } ` A ) ) )
121 fvexd 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. _V )
122 8 121 88 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( { <. A , ( F ` j ) >. } ` A ) = ( F ` j ) )
123 1st2nd2 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( F ` j ) = <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
124 11 123 syl 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
125 122 124 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( { <. A , ( F ` j ) >. } ` A ) = <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
126 125 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( { <. A , ( F ` j ) >. } ` A ) ) = ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) )
127 df-ov 
 |-  ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) = ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
128 127 eqcomi 
 |-  ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) )
129 128 a1i 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
130 126 129 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( { <. A , ( F ` j ) >. } ` A ) ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
131 112 120 130 3eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
132 131 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) = ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) )
133 xp1st 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( 1st ` ( F ` j ) ) e. RR )
134 11 133 syl 
 |-  ( ( ph /\ j e. NN ) -> ( 1st ` ( F ` j ) ) e. RR )
135 xp2nd 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( 2nd ` ( F ` j ) ) e. RR )
136 11 135 syl 
 |-  ( ( ph /\ j e. NN ) -> ( 2nd ` ( F ` j ) ) e. RR )
137 volicore 
 |-  ( ( ( 1st ` ( F ` j ) ) e. RR /\ ( 2nd ` ( F ` j ) ) e. RR ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) e. RR )
138 134 136 137 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) e. RR )
139 132 138 eqeltrd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) e. RR )
140 139 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) e. CC )
141 2fveq3 
 |-  ( k = A -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) )
142 141 prodsn 
 |-  ( ( A e. V /\ ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) e. CC ) -> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) )
143 8 140 142 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) )
144 143 132 eqtr2d 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) = prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
145 144 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) ) = ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
146 109 145 eqtrd 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
147 146 fveq2d 
 |-  ( ph -> ( sum^ ` ( ( vol o. [,) ) o. F ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
148 6 147 eqtrd 
 |-  ( ph -> Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
149 102 148 jca 
 |-  ( ph -> ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) )
150 fveq1 
 |-  ( i = I -> ( i ` j ) = ( I ` j ) )
151 150 coeq2d 
 |-  ( i = I -> ( [,) o. ( i ` j ) ) = ( [,) o. ( I ` j ) ) )
152 151 fveq1d 
 |-  ( i = I -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
153 152 ixpeq2dv 
 |-  ( i = I -> X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) )
154 153 iuneq2d 
 |-  ( i = I -> U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) )
155 154 sseq2d 
 |-  ( i = I -> ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) <-> ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) ) )
156 simpl 
 |-  ( ( i = I /\ k e. { A } ) -> i = I )
157 156 fveq1d 
 |-  ( ( i = I /\ k e. { A } ) -> ( i ` j ) = ( I ` j ) )
158 157 coeq2d 
 |-  ( ( i = I /\ k e. { A } ) -> ( [,) o. ( i ` j ) ) = ( [,) o. ( I ` j ) ) )
159 158 fveq1d 
 |-  ( ( i = I /\ k e. { A } ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
160 159 fveq2d 
 |-  ( ( i = I /\ k e. { A } ) -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
161 160 prodeq2dv 
 |-  ( i = I -> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
162 161 mpteq2dv 
 |-  ( i = I -> ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
163 162 fveq2d 
 |-  ( i = I -> ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
164 163 eqeq2d 
 |-  ( i = I -> ( Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) )
165 155 164 anbi12d 
 |-  ( i = I -> ( ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) ) )
166 165 rspcev 
 |-  ( ( I e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) /\ ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
167 29 149 166 syl2anc 
 |-  ( ph -> E. i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )