Metamath Proof Explorer

Theorem vonvolmbl

Description: A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses vonvolmbl.a 
|- ( ph -> A e. V )
vonvolmbl.b 
|- ( ph -> B C_ RR )
Assertion vonvolmbl 
|- ( ph -> ( ( B ^m { A } ) e. dom ( voln ` { A } ) <-> B e. dom vol ) )

Proof

Step Hyp Ref Expression
1 vonvolmbl.a 
 |-  ( ph -> A e. V )
2 vonvolmbl.b 
 |-  ( ph -> B C_ RR )
3 vex 
 |-  y e. _V
4 3 a1i 
 |-  ( ph -> y e. _V )
5 reex 
 |-  RR e. _V
6 5 a1i 
 |-  ( ph -> RR e. _V )
7 6 2 ssexd 
 |-  ( ph -> B e. _V )
8 snfi 
 |-  { A } e. Fin
9 8 a1i 
 |-  ( ph -> { A } e. Fin )
10 9 elexd 
 |-  ( ph -> { A } e. _V )
11 4 7 10 inmap 
 |-  ( ph -> ( ( y ^m { A } ) i^i ( B ^m { A } ) ) = ( ( y i^i B ) ^m { A } ) )
12 11 eqcomd 
 |-  ( ph -> ( ( y i^i B ) ^m { A } ) = ( ( y ^m { A } ) i^i ( B ^m { A } ) ) )
13 12 fveq2d 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) = ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) )
14 4 7 1 difmapsn 
 |-  ( ph -> ( ( y ^m { A } ) \ ( B ^m { A } ) ) = ( ( y \ B ) ^m { A } ) )
15 14 eqcomd 
 |-  ( ph -> ( ( y \ B ) ^m { A } ) = ( ( y ^m { A } ) \ ( B ^m { A } ) ) )
16 15 fveq2d 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) = ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) )
17 13 16 oveq12d 
 |-  ( ph -> ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) = ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) )
18 17 ad2antrr 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) = ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) )
19 ovexd 
 |-  ( y e. ~P RR -> ( y ^m { A } ) e. _V )
20 5 a1i 
 |-  ( y e. ~P RR -> RR e. _V )
21 elpwi 
 |-  ( y e. ~P RR -> y C_ RR )
22 mapss 
 |-  ( ( RR e. _V /\ y C_ RR ) -> ( y ^m { A } ) C_ ( RR ^m { A } ) )
23 20 21 22 syl2anc 
 |-  ( y e. ~P RR -> ( y ^m { A } ) C_ ( RR ^m { A } ) )
24 19 23 elpwd 
 |-  ( y e. ~P RR -> ( y ^m { A } ) e. ~P ( RR ^m { A } ) )
25 24 adantl 
 |-  ( ( A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) /\ y e. ~P RR ) -> ( y ^m { A } ) e. ~P ( RR ^m { A } ) )
26 simpl 
 |-  ( ( A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) /\ y e. ~P RR ) -> A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) )
27 ineq1 
 |-  ( x = ( y ^m { A } ) -> ( x i^i ( B ^m { A } ) ) = ( ( y ^m { A } ) i^i ( B ^m { A } ) ) )
28 27 fveq2d 
 |-  ( x = ( y ^m { A } ) -> ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) = ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) )
29 difeq1 
 |-  ( x = ( y ^m { A } ) -> ( x \ ( B ^m { A } ) ) = ( ( y ^m { A } ) \ ( B ^m { A } ) ) )
30 29 fveq2d 
 |-  ( x = ( y ^m { A } ) -> ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) = ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) )
31 28 30 oveq12d 
 |-  ( x = ( y ^m { A } ) -> ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) )
32 fveq2 
 |-  ( x = ( y ^m { A } ) -> ( ( voln* ` { A } ) ` x ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
33 31 32 eqeq12d 
 |-  ( x = ( y ^m { A } ) -> ( ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) <-> ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) ) )
34 33 rspcva 
 |-  ( ( ( y ^m { A } ) e. ~P ( RR ^m { A } ) /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) -> ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
35 25 26 34 syl2anc 
 |-  ( ( A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
36 35 adantll 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y ^m { A } ) i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( ( y ^m { A } ) \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
37 eqidd 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( y ^m { A } ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
38 18 36 37 3eqtrd 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) = ( ( voln* ` { A } ) ` ( y ^m { A } ) ) )
39 38 eqcomd 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( y ^m { A } ) ) = ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) )
40 1 adantr 
 |-  ( ( ph /\ y e. ~P RR ) -> A e. V )
41 21 adantl 
 |-  ( ( ph /\ y e. ~P RR ) -> y C_ RR )
42 40 41 ovnovol 
 |-  ( ( ph /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( y ^m { A } ) ) = ( vol* ` y ) )
43 42 adantlr 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( y ^m { A } ) ) = ( vol* ` y ) )
44 41 ssinss1d 
 |-  ( ( ph /\ y e. ~P RR ) -> ( y i^i B ) C_ RR )
45 40 44 ovnovol 
 |-  ( ( ph /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) = ( vol* ` ( y i^i B ) ) )
46 41 ssdifssd 
 |-  ( ( ph /\ y e. ~P RR ) -> ( y \ B ) C_ RR )
47 40 46 ovnovol 
 |-  ( ( ph /\ y e. ~P RR ) -> ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) = ( vol* ` ( y \ B ) ) )
48 45 47 oveq12d 
 |-  ( ( ph /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
49 48 adantlr 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( ( ( voln* ` { A } ) ` ( ( y i^i B ) ^m { A } ) ) +e ( ( voln* ` { A } ) ` ( ( y \ B ) ^m { A } ) ) ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
50 39 43 49 3eqtr3d 
 |-  ( ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) /\ y e. ~P RR ) -> ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
51 50 ralrimiva 
 |-  ( ( ph /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) -> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
52 51 ex 
 |-  ( ph -> ( A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) -> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) )
53 1 ad2antrr 
 |-  ( ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) /\ x e. ~P ( RR ^m { A } ) ) -> A e. V )
54 2 ad2antrr 
 |-  ( ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) /\ x e. ~P ( RR ^m { A } ) ) -> B C_ RR )
55 simplr 
 |-  ( ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) /\ x e. ~P ( RR ^m { A } ) ) -> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
56 elpwi 
 |-  ( x e. ~P ( RR ^m { A } ) -> x C_ ( RR ^m { A } ) )
57 56 adantl 
 |-  ( ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) /\ x e. ~P ( RR ^m { A } ) ) -> x C_ ( RR ^m { A } ) )
58 rneq 
 |-  ( g = f -> ran g = ran f )
59 58 cbviunv 
 |-  U_ g e. x ran g = U_ f e. x ran f
60 53 54 55 57 59 vonvolmbllem 
 |-  ( ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) /\ x e. ~P ( RR ^m { A } ) ) -> ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) )
61 60 ralrimiva 
 |-  ( ( ph /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) -> A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) )
62 61 ex 
 |-  ( ph -> ( A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) -> A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) )
63 52 62 impbid 
 |-  ( ph -> ( A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) <-> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) )
64 mapss 
 |-  ( ( RR e. _V /\ B C_ RR ) -> ( B ^m { A } ) C_ ( RR ^m { A } ) )
65 6 2 64 syl2anc 
 |-  ( ph -> ( B ^m { A } ) C_ ( RR ^m { A } ) )
66 9 isvonmbl 
 |-  ( ph -> ( ( B ^m { A } ) e. dom ( voln ` { A } ) <-> ( ( B ^m { A } ) C_ ( RR ^m { A } ) /\ A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) ) )
67 65 66 mpbirand 
 |-  ( ph -> ( ( B ^m { A } ) e. dom ( voln ` { A } ) <-> A. x e. ~P ( RR ^m { A } ) ( ( ( voln* ` { A } ) ` ( x i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( x \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` x ) ) )
68 ismbl4 
 |-  ( B e. dom vol <-> ( B C_ RR /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) )
69 68 a1i 
 |-  ( ph -> ( B e. dom vol <-> ( B C_ RR /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) ) )
70 2 69 mpbirand 
 |-  ( ph -> ( B e. dom vol <-> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) )
71 63 67 70 3bitr4d 
 |-  ( ph -> ( ( B ^m { A } ) e. dom ( voln ` { A } ) <-> B e. dom vol ) )