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