Theorem mblvon

Description: The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	mblvon.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	mblvon.2	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ 𝑋 ) )
Assertion	mblvon	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mblvon.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		mblvon.2	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ 𝑋 ) )
3	1	vonval	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
4	3	fveq1d	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐴 ) )
5	1	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
6	2 5	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
7		fvres	⊢ ( 𝐴 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) → ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
8	6 7	syl	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
9	4 8	eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )