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	|- ( ph -> X e. Fin )
Assertion	vonval	|- ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonval.1	|- ( ph -> X e. Fin )
2		df-voln	|- voln = ( x e. Fin |-> ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) )
3		fveq2	|- ( x = X -> ( voln* ` x ) = ( voln* ` X ) )
4		2fveq3	|- ( x = X -> ( CaraGen ` ( voln* ` x ) ) = ( CaraGen ` ( voln* ` X ) ) )
5	3 4	reseq12d	|- ( x = X -> ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )
6		fvex	|- ( voln* ` X ) e. _V
7	6	resex	|- ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) e. _V
8	7	a1i	|- ( ph -> ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) e. _V )
9	2 5 1 8	fvmptd3	|- ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )