Metamath Proof Explorer

Theorem ovnlecvr

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. The statement would also be true with X the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnlecvr.x 
|- ( ph -> X e. Fin )
ovnlecvr.n0 
|- ( ph -> X =/= (/) )
ovnlecvr.l 
|- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
ovnlecvr.i 
|- ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )
ovnlecvr.ss 
|- ( ph -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
Assertion ovnlecvr 
|- ( ph -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnlecvr.x 
 |-  ( ph -> X e. Fin )
2 ovnlecvr.n0 
 |-  ( ph -> X =/= (/) )
3 ovnlecvr.l 
 |-  L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
4 ovnlecvr.i 
 |-  ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )
5 ovnlecvr.ss 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
6 4 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) e. ( ( RR X. RR ) ^m X ) )
7 elmapi 
 |-  ( ( I ` j ) e. ( ( RR X. RR ) ^m X ) -> ( I ` j ) : X --> ( RR X. RR ) )
8 6 7 syl 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
9 8 hoissrrn 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) C_ ( RR ^m X ) )
10 9 ralrimiva 
 |-  ( ph -> A. j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) C_ ( RR ^m X ) )
11 iunss 
 |-  ( U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) C_ ( RR ^m X ) <-> A. j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) C_ ( RR ^m X ) )
12 10 11 sylibr 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) C_ ( RR ^m X ) )
13 5 12 sstrd 
 |-  ( ph -> A C_ ( RR ^m X ) )
14 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 ) ) ) ) ) }
15 1 2 13 14 ovnn0val 
 |-  ( ph -> ( ( 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* , < ) )
16 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*
17 16 a1i 
 |-  ( ph -> { 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* )
18 nnex 
 |-  NN e. _V
19 18 a1i 
 |-  ( ph -> NN e. _V )
20 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
21 nfv 
 |-  F/ k ( ph /\ j e. NN )
22 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
23 21 22 3 8 hoiprodcl2 
 |-  ( ( ph /\ j e. NN ) -> ( L ` ( I ` j ) ) e. ( 0 [,) +oo ) )
24 20 23 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( L ` ( I ` j ) ) e. ( 0 [,] +oo ) )
25 eqid 
 |-  ( j e. NN |-> ( L ` ( I ` j ) ) ) = ( j e. NN |-> ( L ` ( I ` j ) ) )
26 24 25 fmptd 
 |-  ( ph -> ( j e. NN |-> ( L ` ( I ` j ) ) ) : NN --> ( 0 [,] +oo ) )
27 19 26 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) e. RR* )
28 ovex 
 |-  ( ( RR X. RR ) ^m X ) e. _V
29 28 18 pm3.2i 
 |-  ( ( ( RR X. RR ) ^m X ) e. _V /\ NN e. _V )
30 elmapg 
 |-  ( ( ( ( RR X. RR ) ^m X ) e. _V /\ NN e. _V ) -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) ) )
31 29 30 ax-mp 
 |-  ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) )
32 4 31 sylibr 
 |-  ( ph -> I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
33 coeq2 
 |-  ( i = ( I ` j ) -> ( [,) o. i ) = ( [,) o. ( I ` j ) ) )
34 33 fveq1d 
 |-  ( i = ( I ` j ) -> ( ( [,) o. i ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
35 34 fveq2d 
 |-  ( i = ( I ` j ) -> ( vol ` ( ( [,) o. i ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
36 35 prodeq2ad 
 |-  ( i = ( I ` j ) -> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
37 prodex 
 |-  prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. _V
38 37 a1i 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. _V )
39 3 36 6 38 fvmptd3 
 |-  ( ( ph /\ j e. NN ) -> ( L ` ( I ` j ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
40 39 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( L ` ( I ` j ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
41 40 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
42 5 41 jca 
 |-  ( ph -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) )
43 nfv 
 |-  F/ k i = I
44 fveq1 
 |-  ( i = I -> ( i ` j ) = ( I ` j ) )
45 44 coeq2d 
 |-  ( i = I -> ( [,) o. ( i ` j ) ) = ( [,) o. ( I ` j ) ) )
46 45 fveq1d 
 |-  ( i = I -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
47 46 adantr 
 |-  ( ( i = I /\ k e. X ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
48 43 47 ixpeq2d 
 |-  ( i = I -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
49 48 iuneq2d 
 |-  ( i = I -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
50 49 sseq2d 
 |-  ( i = I -> ( 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. ( I ` j ) ) ` k ) ) )
51 46 fveq2d 
 |-  ( i = I -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
52 51 prodeq2ad 
 |-  ( i = I -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
53 52 mpteq2dv 
 |-  ( i = I -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
54 53 fveq2d 
 |-  ( i = I -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
55 54 eqeq2d 
 |-  ( i = I -> ( ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) )
56 50 55 anbi12d 
 |-  ( i = I -> ( ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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. ( I ` j ) ) ` k ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) ) )
57 56 rspcev 
 |-  ( ( 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 |-> ( L ` ( I ` j ) ) ) ) = ( 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
58 32 42 57 syl2anc 
 |-  ( ph -> 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
59 27 58 jca 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
60 eqeq1 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
61 60 anbi2d 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
62 61 rexbidv 
 |-  ( z = ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
63 62 elrab 
 |-  ( ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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 |-> ( L ` ( I ` 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 |-> ( L ` ( I ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
64 59 63 sylibr 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( L ` ( I ` 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 ) ) ) ) ) } )
65 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 |-> ( L ` ( I ` 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 |-> ( L ` ( I ` j ) ) ) ) )
66 17 64 65 syl2anc 
 |-  ( ph -> 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 |-> ( L ` ( I ` j ) ) ) ) )
67 15 66 eqbrtrd 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) )