Metamath Proof Explorer

Theorem ovnovollem2

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

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

Proof

Step Hyp Ref Expression
1 ovnovollem2.a 
 |-  ( ph -> A e. V )
2 ovnovollem2.b 
 |-  ( ph -> B e. W )
3 ovnovollem2.i 
 |-  ( ph -> I e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) )
4 ovnovollem2.s 
 |-  ( ph -> ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) )
5 ovnovollem2.z 
 |-  ( ph -> Z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
6 ovnovollem2.f 
 |-  F = ( j e. NN |-> ( ( I ` j ) ` A ) )
7 elmapi 
 |-  ( I e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) -> I : NN --> ( ( RR X. RR ) ^m { A } ) )
8 3 7 syl 
 |-  ( ph -> I : NN --> ( ( RR X. RR ) ^m { A } ) )
9 8 adantr 
 |-  ( ( ph /\ j e. NN ) -> I : NN --> ( ( RR X. RR ) ^m { A } ) )
10 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
11 9 10 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) e. ( ( RR X. RR ) ^m { A } ) )
12 elmapi 
 |-  ( ( I ` j ) e. ( ( RR X. RR ) ^m { A } ) -> ( I ` j ) : { A } --> ( RR X. RR ) )
13 11 12 syl 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : { A } --> ( RR X. RR ) )
14 snidg 
 |-  ( A e. V -> A e. { A } )
15 1 14 syl 
 |-  ( ph -> A e. { A } )
16 15 adantr 
 |-  ( ( ph /\ j e. NN ) -> A e. { A } )
17 13 16 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( ( I ` j ) ` A ) e. ( RR X. RR ) )
18 17 6 fmptd 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
19 reex 
 |-  RR e. _V
20 19 19 xpex 
 |-  ( RR X. RR ) e. _V
21 nnex 
 |-  NN e. _V
22 20 21 elmap 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) <-> F : NN --> ( RR X. RR ) )
23 22 a1i 
 |-  ( ph -> ( F e. ( ( RR X. RR ) ^m NN ) <-> F : NN --> ( RR X. RR ) ) )
24 18 23 mpbird 
 |-  ( ph -> F e. ( ( RR X. RR ) ^m NN ) )
25 elsni 
 |-  ( k e. { A } -> k = A )
26 25 fveq2d 
 |-  ( k e. { A } -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` A ) )
27 26 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` A ) )
28 elmapfun 
 |-  ( ( I ` j ) e. ( ( RR X. RR ) ^m { A } ) -> Fun ( I ` j ) )
29 11 28 syl 
 |-  ( ( ph /\ j e. NN ) -> Fun ( I ` j ) )
30 13 fdmd 
 |-  ( ( ph /\ j e. NN ) -> dom ( I ` j ) = { A } )
31 30 eqcomd 
 |-  ( ( ph /\ j e. NN ) -> { A } = dom ( I ` j ) )
32 16 31 eleqtrd 
 |-  ( ( ph /\ j e. NN ) -> A e. dom ( I ` j ) )
33 fvco 
 |-  ( ( Fun ( I ` j ) /\ A e. dom ( I ` j ) ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( [,) ` ( ( I ` j ) ` A ) ) )
34 29 32 33 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( [,) ` ( ( I ` j ) ` A ) ) )
35 34 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( [,) ` ( ( I ` j ) ` A ) ) )
36 id 
 |-  ( j e. NN -> j e. NN )
37 fvexd 
 |-  ( j e. NN -> ( ( I ` j ) ` A ) e. _V )
38 6 fvmpt2 
 |-  ( ( j e. NN /\ ( ( I ` j ) ` A ) e. _V ) -> ( F ` j ) = ( ( I ` j ) ` A ) )
39 36 37 38 syl2anc 
 |-  ( j e. NN -> ( F ` j ) = ( ( I ` j ) ` A ) )
40 39 eqcomd 
 |-  ( j e. NN -> ( ( I ` j ) ` A ) = ( F ` j ) )
41 40 fveq2d 
 |-  ( j e. NN -> ( [,) ` ( ( I ` j ) ` A ) ) = ( [,) ` ( F ` j ) ) )
42 41 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( ( I ` j ) ` A ) ) = ( [,) ` ( F ` j ) ) )
43 18 ffund 
 |-  ( ph -> Fun F )
44 43 adantr 
 |-  ( ( ph /\ j e. NN ) -> Fun F )
45 6 17 dmmptd 
 |-  ( ph -> dom F = NN )
46 45 eqcomd 
 |-  ( ph -> NN = dom F )
47 46 adantr 
 |-  ( ( ph /\ j e. NN ) -> NN = dom F )
48 10 47 eleqtrd 
 |-  ( ( ph /\ j e. NN ) -> j e. dom F )
49 fvco 
 |-  ( ( Fun F /\ j e. dom F ) -> ( ( [,) o. F ) ` j ) = ( [,) ` ( F ` j ) ) )
50 44 48 49 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. F ) ` j ) = ( [,) ` ( F ` j ) ) )
51 50 eqcomd 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( F ` j ) ) = ( ( [,) o. F ) ` j ) )
52 42 51 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( ( I ` j ) ` A ) ) = ( ( [,) o. F ) ` j ) )
53 52 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( [,) ` ( ( I ` j ) ` A ) ) = ( ( [,) o. F ) ` j ) )
54 27 35 53 3eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. { A } ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( [,) o. F ) ` j ) )
55 54 ixpeq2dva 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = X_ k e. { A } ( ( [,) o. F ) ` j ) )
56 snex 
 |-  { A } e. _V
57 fvex 
 |-  ( ( [,) o. F ) ` j ) e. _V
58 56 57 ixpconst 
 |-  X_ k e. { A } ( ( [,) o. F ) ` j ) = ( ( ( [,) o. F ) ` j ) ^m { A } )
59 58 a1i 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( ( [,) o. F ) ` j ) = ( ( ( [,) o. F ) ` j ) ^m { A } ) )
60 55 59 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = ( ( ( [,) o. F ) ` j ) ^m { A } ) )
61 60 iuneq2dv 
 |-  ( ph -> U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = U_ j e. NN ( ( ( [,) o. F ) ` j ) ^m { A } ) )
62 nfv 
 |-  F/ j ph
63 21 a1i 
 |-  ( ph -> NN e. _V )
64 fvexd 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. F ) ` j ) e. _V )
65 62 63 64 1 iunmapsn 
 |-  ( ph -> U_ j e. NN ( ( ( [,) o. F ) ` j ) ^m { A } ) = ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) )
66 61 65 eqtrd 
 |-  ( ph -> U_ j e. NN X_ k e. { A } ( ( [,) o. ( I ` j ) ) ` k ) = ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) )
67 4 66 sseqtrd 
 |-  ( ph -> ( B ^m { A } ) C_ ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) )
68 21 57 iunex 
 |-  U_ j e. NN ( ( [,) o. F ) ` j ) e. _V
69 68 a1i 
 |-  ( ph -> U_ j e. NN ( ( [,) o. F ) ` j ) e. _V )
70 56 a1i 
 |-  ( ph -> { A } e. _V )
71 15 ne0d 
 |-  ( ph -> { A } =/= (/) )
72 2 69 70 71 mapss2 
 |-  ( ph -> ( B C_ U_ j e. NN ( ( [,) o. F ) ` j ) <-> ( B ^m { A } ) C_ ( U_ j e. NN ( ( [,) o. F ) ` j ) ^m { A } ) ) )
73 67 72 mpbird 
 |-  ( ph -> B C_ U_ j e. NN ( ( [,) o. F ) ` j ) )
74 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
75 74 a1i 
 |-  ( ph -> [,) : ( RR* X. RR* ) --> ~P RR* )
76 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
77 76 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR* X. RR* ) )
78 75 77 18 fcoss 
 |-  ( ph -> ( [,) o. F ) : NN --> ~P RR* )
79 78 ffnd 
 |-  ( ph -> ( [,) o. F ) Fn NN )
80 fniunfv 
 |-  ( ( [,) o. F ) Fn NN -> U_ j e. NN ( ( [,) o. F ) ` j ) = U. ran ( [,) o. F ) )
81 79 80 syl 
 |-  ( ph -> U_ j e. NN ( ( [,) o. F ) ` j ) = U. ran ( [,) o. F ) )
82 73 81 sseqtrd 
 |-  ( ph -> B C_ U. ran ( [,) o. F ) )
83 nfcv 
 |-  F/_ j F
84 ressxr 
 |-  RR C_ RR*
85 xpss2 
 |-  ( RR C_ RR* -> ( RR X. RR ) C_ ( RR X. RR* ) )
86 84 85 ax-mp 
 |-  ( RR X. RR ) C_ ( RR X. RR* )
87 86 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR X. RR* ) )
88 18 87 fssd 
 |-  ( ph -> F : NN --> ( RR X. RR* ) )
89 83 88 volicofmpt 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( j e. NN |-> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) ) )
90 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> A e. V )
91 fvexd 
 |-  ( ( ph /\ j e. NN ) -> ( ( I ` j ) ` A ) e. _V )
92 10 91 38 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = ( ( I ` j ) ` A ) )
93 92 17 eqeltrd 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR X. RR ) )
94 1st2nd2 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( F ` j ) = <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
95 93 94 syl 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
96 95 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` ( F ` j ) ) = ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) )
97 df-ov 
 |-  ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) = ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. )
98 97 eqcomi 
 |-  ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) )
99 98 a1i 
 |-  ( ( ph /\ j e. NN ) -> ( [,) ` <. ( 1st ` ( F ` j ) ) , ( 2nd ` ( F ` j ) ) >. ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
100 50 96 99 3eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. F ) ` j ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
101 34 52 100 3eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( [,) o. ( I ` j ) ) ` A ) = ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) )
102 101 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) = ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) )
103 xp1st 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( 1st ` ( F ` j ) ) e. RR )
104 93 103 syl 
 |-  ( ( ph /\ j e. NN ) -> ( 1st ` ( F ` j ) ) e. RR )
105 xp2nd 
 |-  ( ( F ` j ) e. ( RR X. RR ) -> ( 2nd ` ( F ` j ) ) e. RR )
106 93 105 syl 
 |-  ( ( ph /\ j e. NN ) -> ( 2nd ` ( F ` j ) ) e. RR )
107 volicore 
 |-  ( ( ( 1st ` ( F ` j ) ) e. RR /\ ( 2nd ` ( F ` j ) ) e. RR ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) e. RR )
108 104 106 107 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) e. RR )
109 102 108 eqeltrd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) e. RR )
110 109 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) e. CC )
111 2fveq3 
 |-  ( k = A -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) )
112 111 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 ) ) )
113 90 110 112 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` A ) ) )
114 113 102 eqtr2d 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) = prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
115 114 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( 1st ` ( F ` j ) ) [,) ( 2nd ` ( F ` j ) ) ) ) ) = ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
116 89 115 eqtrd 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
117 116 fveq2d 
 |-  ( ph -> ( sum^ ` ( ( vol o. [,) ) o. F ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
118 5 117 eqtr4d 
 |-  ( ph -> Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
119 82 118 jca 
 |-  ( ph -> ( B C_ U. ran ( [,) o. F ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) ) )
120 coeq2 
 |-  ( f = F -> ( [,) o. f ) = ( [,) o. F ) )
121 120 rneqd 
 |-  ( f = F -> ran ( [,) o. f ) = ran ( [,) o. F ) )
122 121 unieqd 
 |-  ( f = F -> U. ran ( [,) o. f ) = U. ran ( [,) o. F ) )
123 122 sseq2d 
 |-  ( f = F -> ( B C_ U. ran ( [,) o. f ) <-> B C_ U. ran ( [,) o. F ) ) )
124 coeq2 
 |-  ( f = F -> ( ( vol o. [,) ) o. f ) = ( ( vol o. [,) ) o. F ) )
125 124 fveq2d 
 |-  ( f = F -> ( sum^ ` ( ( vol o. [,) ) o. f ) ) = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
126 125 eqeq2d 
 |-  ( f = F -> ( Z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) <-> Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) ) )
127 123 126 anbi12d 
 |-  ( f = F -> ( ( B C_ U. ran ( [,) o. f ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) <-> ( B C_ U. ran ( [,) o. F ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) ) ) )
128 127 rspcev 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ ( B C_ U. ran ( [,) o. F ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. F ) ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
129 24 119 128 syl2anc 
 |-  ( ph -> E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ Z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )