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* ‘ { 𝐴 } ) ‘ 𝑋 ) )