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	|- ( ph -> X e. Fin )
	mblvon.2	|- ( ph -> A e. dom ( voln ` X ) )
Assertion	mblvon	|- ( ph -> ( ( voln ` X ) ` A ) = ( ( voln* ` X ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		mblvon.1	|- ( ph -> X e. Fin )
2		mblvon.2	|- ( ph -> A e. dom ( voln ` X ) )
3	1	vonval	|- ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )
4	3	fveq1d	|- ( ph -> ( ( voln ` X ) ` A ) = ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` A ) )
5	1	dmvon	|- ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
6	2 5	eleqtrd	|- ( ph -> A e. ( CaraGen ` ( voln* ` X ) ) )
7		fvres	|- ( A e. ( CaraGen ` ( voln* ` X ) ) -> ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` A ) = ( ( voln* ` X ) ` A ) )
8	6 7	syl	|- ( ph -> ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` A ) = ( ( voln* ` X ) ` A ) )
9	4 8	eqtrd	|- ( ph -> ( ( voln ` X ) ` A ) = ( ( voln* ` X ) ` A ) )