Theorem vonvol

Description: The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	vonvol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	vonvol.b	⊢ ( 𝜑 → 𝐵 ∈ dom vol )
Assertion	vonvol	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		vonvol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		vonvol.b	⊢ ( 𝜑 → 𝐵 ∈ dom vol )
3		mblss	⊢ ( 𝐵 ∈ dom vol → 𝐵 ⊆ ℝ )
4	2 3	syl	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
5	1 4	ovnovol	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )
6		snfi	⊢ { 𝐴 } ∈ Fin
7	6	a1i	⊢ ( 𝜑 → { 𝐴 } ∈ Fin )
8	1 4	vonvolmbl	⊢ ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝐵 ∈ dom vol ) )
9	2 8	mpbird	⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) )
10	7 9	mblvon	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) )
11		mblvol	⊢ ( 𝐵 ∈ dom vol → ( vol ‘ 𝐵 ) = ( vol* ‘ 𝐵 ) )
12	2 11	syl	⊢ ( 𝜑 → ( vol ‘ 𝐵 ) = ( vol* ‘ 𝐵 ) )
13	5 10 12	3eqtr4d	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol ‘ 𝐵 ) )