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 ( 𝜑𝐴𝑉 )
vonvolmbllem.b ( 𝜑𝐵 ⊆ ℝ )
vonvolmbllem.e ( 𝜑 → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦𝐵 ) ) ) )
vonvolmbllem.x ( 𝜑𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
vonvolmbllem.y 𝑌 = 𝑓𝑋 ran 𝑓
Assertion vonvolmbllem ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 vonvolmbllem.a ( 𝜑𝐴𝑉 )
2 vonvolmbllem.b ( 𝜑𝐵 ⊆ ℝ )
3 vonvolmbllem.e ( 𝜑 → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦𝐵 ) ) ) )
4 vonvolmbllem.x ( 𝜑𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
5 vonvolmbllem.y 𝑌 = 𝑓𝑋 ran 𝑓
6 nfcv 𝑓 𝑌
7 6 1 4 5 ssmapsn ( 𝜑𝑋 = ( 𝑌m { 𝐴 } ) )
8 7 ineq1d ( 𝜑 → ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌m { 𝐴 } ) ∩ ( 𝐵m { 𝐴 } ) ) )
9 reex ℝ ∈ V
10 9 a1i ( 𝜑 → ℝ ∈ V )
11 4 sselda ( ( 𝜑𝑓𝑋 ) → 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) )
12 elmapi ( 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ ℝ )
13 11 12 syl ( ( 𝜑𝑓𝑋 ) → 𝑓 : { 𝐴 } ⟶ ℝ )
14 13 frnd ( ( 𝜑𝑓𝑋 ) → ran 𝑓 ⊆ ℝ )
15 14 ralrimiva ( 𝜑 → ∀ 𝑓𝑋 ran 𝑓 ⊆ ℝ )
16 iunss ( 𝑓𝑋 ran 𝑓 ⊆ ℝ ↔ ∀ 𝑓𝑋 ran 𝑓 ⊆ ℝ )
17 15 16 sylibr ( 𝜑 𝑓𝑋 ran 𝑓 ⊆ ℝ )
18 5 17 eqsstrid ( 𝜑𝑌 ⊆ ℝ )
19 10 18 ssexd ( 𝜑𝑌 ∈ V )
20 10 2 ssexd ( 𝜑𝐵 ∈ V )
21 snex { 𝐴 } ∈ V
22 21 a1i ( 𝜑 → { 𝐴 } ∈ V )
23 19 20 22 inmap ( 𝜑 → ( ( 𝑌m { 𝐴 } ) ∩ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) )
24 8 23 eqtrd ( 𝜑 → ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) )
25 24 fveq2d ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) ) )
26 18 ssinss1d ( 𝜑 → ( 𝑌𝐵 ) ⊆ ℝ )
27 1 26 ovnovol ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
28 25 27 eqtrd ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
29 7 difeq1d ( 𝜑 → ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌m { 𝐴 } ) ∖ ( 𝐵m { 𝐴 } ) ) )
30 19 20 1 difmapsn ( 𝜑 → ( ( 𝑌m { 𝐴 } ) ∖ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) )
31 29 30 eqtrd ( 𝜑 → ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) = ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) )
32 31 fveq2d ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) ) )
33 18 ssdifssd ( 𝜑 → ( 𝑌𝐵 ) ⊆ ℝ )
34 1 33 ovnovol ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
35 32 34 eqtrd ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
36 28 35 oveq12d ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) ) ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) )
37 7 fveq2d ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑌m { 𝐴 } ) ) )
38 1 18 ovnovol ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑌m { 𝐴 } ) ) = ( vol* ‘ 𝑌 ) )
39 19 18 elpwd ( 𝜑𝑌 ∈ 𝒫 ℝ )
40 fveq2 ( 𝑦 = 𝑌 → ( vol* ‘ 𝑦 ) = ( vol* ‘ 𝑌 ) )
41 ineq1 ( 𝑦 = 𝑌 → ( 𝑦𝐵 ) = ( 𝑌𝐵 ) )
42 41 fveq2d ( 𝑦 = 𝑌 → ( vol* ‘ ( 𝑦𝐵 ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
43 difeq1 ( 𝑦 = 𝑌 → ( 𝑦𝐵 ) = ( 𝑌𝐵 ) )
44 43 fveq2d ( 𝑦 = 𝑌 → ( vol* ‘ ( 𝑦𝐵 ) ) = ( vol* ‘ ( 𝑌𝐵 ) ) )
45 42 44 oveq12d ( 𝑦 = 𝑌 → ( ( vol* ‘ ( 𝑦𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦𝐵 ) ) ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) )
46 40 45 eqeq12d ( 𝑦 = 𝑌 → ( ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦𝐵 ) ) ) ↔ ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) ) )
47 46 rspcva ( ( 𝑌 ∈ 𝒫 ℝ ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦𝐵 ) ) ) ) → ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) )
48 39 3 47 syl2anc ( 𝜑 → ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) )
49 37 38 48 3eqtrd ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) = ( ( vol* ‘ ( 𝑌𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌𝐵 ) ) ) )
50 36 49 eqtr4d ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) )