Metamath Proof Explorer

Theorem ovnlerp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnlerp.x 
|- ( ph -> X e. Fin )
ovnlerp.n0 
|- ( ph -> X =/= (/) )
ovnlerp.a 
|- ( ph -> A C_ ( RR ^m X ) )
ovnlerp.e 
|- ( ph -> E e. RR+ )
ovnlerp.m 
|- M = { 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 ) ) ) ) ) }
Assertion ovnlerp 
|- ( ph -> E. z e. M z <_ ( ( ( voln* ` X ) ` A ) +e E ) )

Proof

Step Hyp Ref Expression
1 ovnlerp.x 
 |-  ( ph -> X e. Fin )
2 ovnlerp.n0 
 |-  ( ph -> X =/= (/) )
3 ovnlerp.a 
 |-  ( ph -> A C_ ( RR ^m X ) )
4 ovnlerp.e 
 |-  ( ph -> E e. RR+ )
5 ovnlerp.m 
 |-  M = { 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 ) ) ) ) ) }
6 nfv 
 |-  F/ x ph
7 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*
8 5 7 eqsstri 
 |-  M C_ RR*
9 8 a1i 
 |-  ( ph -> M C_ RR* )
10 1 3 5 ovnpnfelsup 
 |-  ( ph -> +oo e. M )
11 10 ne0d 
 |-  ( ph -> M =/= (/) )
12 0red 
 |-  ( ph -> 0 e. RR )
13 1 3 5 ovnsupge0 
 |-  ( ph -> M C_ ( 0 [,] +oo ) )
14 0xr 
 |-  0 e. RR*
15 14 a1i 
 |-  ( ( M C_ ( 0 [,] +oo ) /\ y e. M ) -> 0 e. RR* )
16 pnfxr 
 |-  +oo e. RR*
17 16 a1i 
 |-  ( ( M C_ ( 0 [,] +oo ) /\ y e. M ) -> +oo e. RR* )
18 ssel2 
 |-  ( ( M C_ ( 0 [,] +oo ) /\ y e. M ) -> y e. ( 0 [,] +oo ) )
19 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ y e. ( 0 [,] +oo ) ) -> 0 <_ y )
20 15 17 18 19 syl3anc 
 |-  ( ( M C_ ( 0 [,] +oo ) /\ y e. M ) -> 0 <_ y )
21 20 ralrimiva 
 |-  ( M C_ ( 0 [,] +oo ) -> A. y e. M 0 <_ y )
22 13 21 syl 
 |-  ( ph -> A. y e. M 0 <_ y )
23 breq1 
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
24 23 ralbidv 
 |-  ( x = 0 -> ( A. y e. M x <_ y <-> A. y e. M 0 <_ y ) )
25 24 rspcev 
 |-  ( ( 0 e. RR /\ A. y e. M 0 <_ y ) -> E. x e. RR A. y e. M x <_ y )
26 12 22 25 syl2anc 
 |-  ( ph -> E. x e. RR A. y e. M x <_ y )
27 6 9 11 26 4 infrpge 
 |-  ( ph -> E. w e. M w <_ ( inf ( M , RR* , < ) +e E ) )
28 nfv 
 |-  F/ w ph
29 simp3 
 |-  ( ( ph /\ w e. M /\ w <_ ( inf ( M , RR* , < ) +e E ) ) -> w <_ ( inf ( M , RR* , < ) +e E ) )
30 1 2 3 5 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` A ) = inf ( M , RR* , < ) )
31 30 eqcomd 
 |-  ( ph -> inf ( M , RR* , < ) = ( ( voln* ` X ) ` A ) )
32 31 oveq1d 
 |-  ( ph -> ( inf ( M , RR* , < ) +e E ) = ( ( ( voln* ` X ) ` A ) +e E ) )
33 32 3ad2ant1 
 |-  ( ( ph /\ w e. M /\ w <_ ( inf ( M , RR* , < ) +e E ) ) -> ( inf ( M , RR* , < ) +e E ) = ( ( ( voln* ` X ) ` A ) +e E ) )
34 29 33 breqtrd 
 |-  ( ( ph /\ w e. M /\ w <_ ( inf ( M , RR* , < ) +e E ) ) -> w <_ ( ( ( voln* ` X ) ` A ) +e E ) )
35 34 3exp 
 |-  ( ph -> ( w e. M -> ( w <_ ( inf ( M , RR* , < ) +e E ) -> w <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) )
36 28 35 reximdai 
 |-  ( ph -> ( E. w e. M w <_ ( inf ( M , RR* , < ) +e E ) -> E. w e. M w <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
37 27 36 mpd 
 |-  ( ph -> E. w e. M w <_ ( ( ( voln* ` X ) ` A ) +e E ) )
38 nfcv 
 |-  F/_ w M
39 nfrab1 
 |-  F/_ z { 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 ) ) ) ) ) }
40 5 39 nfcxfr 
 |-  F/_ z M
41 nfv 
 |-  F/ z w <_ ( ( ( voln* ` X ) ` A ) +e E )
42 nfv 
 |-  F/ w z <_ ( ( ( voln* ` X ) ` A ) +e E )
43 breq1 
 |-  ( w = z -> ( w <_ ( ( ( voln* ` X ) ` A ) +e E ) <-> z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
44 38 40 41 42 43 cbvrexfw 
 |-  ( E. w e. M w <_ ( ( ( voln* ` X ) ` A ) +e E ) <-> E. z e. M z <_ ( ( ( voln* ` X ) ` A ) +e E ) )
45 37 44 sylib 
 |-  ( ph -> E. z e. M z <_ ( ( ( voln* ` X ) ` A ) +e E ) )