Theorem vonval

Description: Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	vonval.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	vonval	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonval.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		df-voln	⊢ voln = ( 𝑥 ∈ Fin ↦ ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) )
3		fveq2	⊢ ( 𝑥 = 𝑋 → ( voln* ‘ 𝑥 ) = ( voln* ‘ 𝑋 ) )
4		2fveq3	⊢ ( 𝑥 = 𝑋 → ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
5	3 4	reseq12d	⊢ ( 𝑥 = 𝑋 → ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
6		fvex	⊢ ( voln* ‘ 𝑋 ) ∈ V
7	6	resex	⊢ ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ∈ V
8	7	a1i	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ∈ V )
9	2 5 1 8	fvmptd3	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )