Metamath Proof Explorer

Theorem ovnovollem3

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnovollem3.a 
|- ( ph -> A e. V )
ovnovollem3.b 
|- ( ph -> B C_ RR )
ovnovollem3.m 
|- M = { z e. RR* | 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 ) ) ) ) ) }
ovnovollem3.n 
|- N = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
Assertion ovnovollem3 
|- ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = ( vol* ` B ) )

Proof

Step Hyp Ref Expression
1 ovnovollem3.a 
 |-  ( ph -> A e. V )
2 ovnovollem3.b 
 |-  ( ph -> B C_ RR )
3 ovnovollem3.m 
 |-  M = { z e. RR* | 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 ) ) ) ) ) }
4 ovnovollem3.n 
 |-  N = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
5 1 snn0d 
 |-  ( ph -> { A } =/= (/) )
6 5 neneqd 
 |-  ( ph -> -. { A } = (/) )
7 6 iffalsed 
 |-  ( ph -> if ( { A } = (/) , 0 , inf ( M , RR* , < ) ) = inf ( M , RR* , < ) )
8 snfi 
 |-  { A } e. Fin
9 8 a1i 
 |-  ( ph -> { A } e. Fin )
10 reex 
 |-  RR e. _V
11 10 a1i 
 |-  ( ph -> RR e. _V )
12 mapss 
 |-  ( ( RR e. _V /\ B C_ RR ) -> ( B ^m { A } ) C_ ( RR ^m { A } ) )
13 11 2 12 syl2anc 
 |-  ( ph -> ( B ^m { A } ) C_ ( RR ^m { A } ) )
14 9 13 3 ovnval2 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = if ( { A } = (/) , 0 , inf ( M , RR* , < ) ) )
15 2 4 ovolval5 
 |-  ( ph -> ( vol* ` B ) = inf ( N , RR* , < ) )
16 1 ad2antrr 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> A e. V )
17 simplr 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> f e. ( ( RR X. RR ) ^m NN ) )
18 fveq2 
 |-  ( n = j -> ( f ` n ) = ( f ` j ) )
19 18 opeq2d 
 |-  ( n = j -> <. A , ( f ` n ) >. = <. A , ( f ` j ) >. )
20 19 sneqd 
 |-  ( n = j -> { <. A , ( f ` n ) >. } = { <. A , ( f ` j ) >. } )
21 20 cbvmptv 
 |-  ( n e. NN |-> { <. A , ( f ` n ) >. } ) = ( j e. NN |-> { <. A , ( f ` j ) >. } )
22 simprl 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> B C_ U. ran ( [,) o. f ) )
23 11 2 ssexd 
 |-  ( ph -> B e. _V )
24 23 adantr 
 |-  ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) -> B e. _V )
25 24 adantr 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> B e. _V )
26 simprr 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
27 16 17 21 22 25 26 ovnovollem1 
 |-  ( ( ( ph /\ f e. ( ( RR X. RR ) ^m NN ) ) /\ ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> 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 ) ) ) ) ) )
28 27 rexlimdva2 
 |-  ( ph -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) -> 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 ) ) ) ) ) ) )
29 1 3ad2ant1 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> A e. V )
30 23 3ad2ant1 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> B e. _V )
31 simp2 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) )
32 simp3l 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) )
33 fveq2 
 |-  ( j = n -> ( i ` j ) = ( i ` n ) )
34 33 coeq2d 
 |-  ( j = n -> ( [,) o. ( i ` j ) ) = ( [,) o. ( i ` n ) ) )
35 34 fveq1d 
 |-  ( j = n -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( i ` n ) ) ` k ) )
36 35 ixpeq2dv 
 |-  ( j = n -> X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. { A } ( ( [,) o. ( i ` n ) ) ` k ) )
37 fveq2 
 |-  ( k = l -> ( ( [,) o. ( i ` n ) ) ` k ) = ( ( [,) o. ( i ` n ) ) ` l ) )
38 37 cbvixpv 
 |-  X_ k e. { A } ( ( [,) o. ( i ` n ) ) ` k ) = X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l )
39 38 a1i 
 |-  ( j = n -> X_ k e. { A } ( ( [,) o. ( i ` n ) ) ` k ) = X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l ) )
40 36 39 eqtrd 
 |-  ( j = n -> X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) = X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l ) )
41 40 cbviunv 
 |-  U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) = U_ n e. NN X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l )
42 41 sseq2i 
 |-  ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) <-> ( B ^m { A } ) C_ U_ n e. NN X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l ) )
43 42 biimpi 
 |-  ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) -> ( B ^m { A } ) C_ U_ n e. NN X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l ) )
44 32 43 syl 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> ( B ^m { A } ) C_ U_ n e. NN X_ l e. { A } ( ( [,) o. ( i ` n ) ) ` l ) )
45 simp3r 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
46 35 fveq2d 
 |-  ( j = n -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( i ` n ) ) ` k ) ) )
47 46 prodeq2ad 
 |-  ( j = n -> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` k ) ) )
48 37 fveq2d 
 |-  ( k = l -> ( vol ` ( ( [,) o. ( i ` n ) ) ` k ) ) = ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) )
49 48 cbvprodv 
 |-  prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` k ) ) = prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) )
50 49 a1i 
 |-  ( j = n -> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` k ) ) = prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) )
51 47 50 eqtrd 
 |-  ( j = n -> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) )
52 51 cbvmptv 
 |-  ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( n e. NN |-> prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) )
53 52 fveq2i 
 |-  ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( n e. NN |-> prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) ) )
54 53 eqeq2i 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> z = ( sum^ ` ( n e. NN |-> prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) ) ) )
55 54 biimpi 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> z = ( sum^ ` ( n e. NN |-> prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) ) ) )
56 45 55 syl 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> z = ( sum^ ` ( n e. NN |-> prod_ l e. { A } ( vol ` ( ( [,) o. ( i ` n ) ) ` l ) ) ) ) )
57 fveq2 
 |-  ( m = n -> ( i ` m ) = ( i ` n ) )
58 57 fveq1d 
 |-  ( m = n -> ( ( i ` m ) ` A ) = ( ( i ` n ) ` A ) )
59 58 cbvmptv 
 |-  ( m e. NN |-> ( ( i ` m ) ` A ) ) = ( n e. NN |-> ( ( i ` n ) ` A ) )
60 29 30 31 44 56 59 ovnovollem2 
 |-  ( ( ph /\ 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. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
61 60 3exp 
 |-  ( ph -> ( 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. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) ) )
62 61 rexlimdv 
 |-  ( 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 ) ) ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
63 28 62 impbid 
 |-  ( ph -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) <-> 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 ) ) ) ) ) ) )
64 63 rabbidv 
 |-  ( ph -> { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) } = { z e. RR* | 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 ) ) ) ) ) } )
65 4 a1i 
 |-  ( ph -> N = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) } )
66 3 a1i 
 |-  ( ph -> M = { z e. RR* | 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 ) ) ) ) ) } )
67 64 65 66 3eqtr4d 
 |-  ( ph -> N = M )
68 67 infeq1d 
 |-  ( ph -> inf ( N , RR* , < ) = inf ( M , RR* , < ) )
69 15 68 eqtrd 
 |-  ( ph -> ( vol* ` B ) = inf ( M , RR* , < ) )
70 7 14 69 3eqtr4d 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = ( vol* ` B ) )