Theorem mzpval

Description: Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpval	|- ( V e. _V -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )

Proof

Step	Hyp	Ref	Expression
1		mzpcln0	|- ( V e. _V -> ( mzPolyCld ` V ) =/= (/) )
2		intex	|- ( ( mzPolyCld ` V ) =/= (/) <-> |^| ( mzPolyCld ` V ) e. _V )
3	1 2	sylib	|- ( V e. _V -> |^| ( mzPolyCld ` V ) e. _V )
4		fveq2	|- ( v = V -> ( mzPolyCld ` v ) = ( mzPolyCld ` V ) )
5	4	inteqd	|- ( v = V -> |^| ( mzPolyCld ` v ) = |^| ( mzPolyCld ` V ) )
6		df-mzp	|- mzPoly = ( v e. _V |-> |^| ( mzPolyCld ` v ) )
7	5 6	fvmptg	|- ( ( V e. _V /\ |^| ( mzPolyCld ` V ) e. _V ) -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )
8	3 7	mpdan	|- ( V e. _V -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )