Metamath Proof Explorer

Theorem vonvolmbllem

Description: If a subset B of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with n equal to 1 ). (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses vonvolmbllem.a 
|- ( ph -> A e. V )
vonvolmbllem.b 
|- ( ph -> B C_ RR )
vonvolmbllem.e 
|- ( ph -> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
vonvolmbllem.x 
|- ( ph -> X C_ ( RR ^m { A } ) )
vonvolmbllem.y 
|- Y = U_ f e. X ran f
Assertion vonvolmbllem 
|- ( ph -> ( ( ( voln* ` { A } ) ` ( X i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( X \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` X ) )

Proof

Step Hyp Ref Expression
1 vonvolmbllem.a 
 |-  ( ph -> A e. V )
2 vonvolmbllem.b 
 |-  ( ph -> B C_ RR )
3 vonvolmbllem.e 
 |-  ( ph -> A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) )
4 vonvolmbllem.x 
 |-  ( ph -> X C_ ( RR ^m { A } ) )
5 vonvolmbllem.y 
 |-  Y = U_ f e. X ran f
6 nfcv 
 |-  F/_ f Y
7 6 1 4 5 ssmapsn 
 |-  ( ph -> X = ( Y ^m { A } ) )
8 7 ineq1d 
 |-  ( ph -> ( X i^i ( B ^m { A } ) ) = ( ( Y ^m { A } ) i^i ( B ^m { A } ) ) )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 4 sselda 
 |-  ( ( ph /\ f e. X ) -> f e. ( RR ^m { A } ) )
12 elmapi 
 |-  ( f e. ( RR ^m { A } ) -> f : { A } --> RR )
13 11 12 syl 
 |-  ( ( ph /\ f e. X ) -> f : { A } --> RR )
14 13 frnd 
 |-  ( ( ph /\ f e. X ) -> ran f C_ RR )
15 14 ralrimiva 
 |-  ( ph -> A. f e. X ran f C_ RR )
16 iunss 
 |-  ( U_ f e. X ran f C_ RR <-> A. f e. X ran f C_ RR )
17 15 16 sylibr 
 |-  ( ph -> U_ f e. X ran f C_ RR )
18 5 17 eqsstrid 
 |-  ( ph -> Y C_ RR )
19 10 18 ssexd 
 |-  ( ph -> Y e. _V )
20 10 2 ssexd 
 |-  ( ph -> B e. _V )
21 snex 
 |-  { A } e. _V
22 21 a1i 
 |-  ( ph -> { A } e. _V )
23 19 20 22 inmap 
 |-  ( ph -> ( ( Y ^m { A } ) i^i ( B ^m { A } ) ) = ( ( Y i^i B ) ^m { A } ) )
24 8 23 eqtrd 
 |-  ( ph -> ( X i^i ( B ^m { A } ) ) = ( ( Y i^i B ) ^m { A } ) )
25 24 fveq2d 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( X i^i ( B ^m { A } ) ) ) = ( ( voln* ` { A } ) ` ( ( Y i^i B ) ^m { A } ) ) )
26 18 ssinss1d 
 |-  ( ph -> ( Y i^i B ) C_ RR )
27 1 26 ovnovol 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( ( Y i^i B ) ^m { A } ) ) = ( vol* ` ( Y i^i B ) ) )
28 25 27 eqtrd 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( X i^i ( B ^m { A } ) ) ) = ( vol* ` ( Y i^i B ) ) )
29 7 difeq1d 
 |-  ( ph -> ( X \ ( B ^m { A } ) ) = ( ( Y ^m { A } ) \ ( B ^m { A } ) ) )
30 19 20 1 difmapsn 
 |-  ( ph -> ( ( Y ^m { A } ) \ ( B ^m { A } ) ) = ( ( Y \ B ) ^m { A } ) )
31 29 30 eqtrd 
 |-  ( ph -> ( X \ ( B ^m { A } ) ) = ( ( Y \ B ) ^m { A } ) )
32 31 fveq2d 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( X \ ( B ^m { A } ) ) ) = ( ( voln* ` { A } ) ` ( ( Y \ B ) ^m { A } ) ) )
33 18 ssdifssd 
 |-  ( ph -> ( Y \ B ) C_ RR )
34 1 33 ovnovol 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( ( Y \ B ) ^m { A } ) ) = ( vol* ` ( Y \ B ) ) )
35 32 34 eqtrd 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( X \ ( B ^m { A } ) ) ) = ( vol* ` ( Y \ B ) ) )
36 28 35 oveq12d 
 |-  ( ph -> ( ( ( voln* ` { A } ) ` ( X i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( X \ ( B ^m { A } ) ) ) ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) )
37 7 fveq2d 
 |-  ( ph -> ( ( voln* ` { A } ) ` X ) = ( ( voln* ` { A } ) ` ( Y ^m { A } ) ) )
38 1 18 ovnovol 
 |-  ( ph -> ( ( voln* ` { A } ) ` ( Y ^m { A } ) ) = ( vol* ` Y ) )
39 19 18 elpwd 
 |-  ( ph -> Y e. ~P RR )
40 fveq2 
 |-  ( y = Y -> ( vol* ` y ) = ( vol* ` Y ) )
41 ineq1 
 |-  ( y = Y -> ( y i^i B ) = ( Y i^i B ) )
42 41 fveq2d 
 |-  ( y = Y -> ( vol* ` ( y i^i B ) ) = ( vol* ` ( Y i^i B ) ) )
43 difeq1 
 |-  ( y = Y -> ( y \ B ) = ( Y \ B ) )
44 43 fveq2d 
 |-  ( y = Y -> ( vol* ` ( y \ B ) ) = ( vol* ` ( Y \ B ) ) )
45 42 44 oveq12d 
 |-  ( y = Y -> ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) )
46 40 45 eqeq12d 
 |-  ( y = Y -> ( ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) <-> ( vol* ` Y ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) ) )
47 46 rspcva 
 |-  ( ( Y e. ~P RR /\ A. y e. ~P RR ( vol* ` y ) = ( ( vol* ` ( y i^i B ) ) +e ( vol* ` ( y \ B ) ) ) ) -> ( vol* ` Y ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) )
48 39 3 47 syl2anc 
 |-  ( ph -> ( vol* ` Y ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) )
49 37 38 48 3eqtrd 
 |-  ( ph -> ( ( voln* ` { A } ) ` X ) = ( ( vol* ` ( Y i^i B ) ) +e ( vol* ` ( Y \ B ) ) ) )
50 36 49 eqtr4d 
 |-  ( ph -> ( ( ( voln* ` { A } ) ` ( X i^i ( B ^m { A } ) ) ) +e ( ( voln* ` { A } ) ` ( X \ ( B ^m { A } ) ) ) ) = ( ( voln* ` { A } ) ` X ) )