Theorem coeid2

Description: Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	|- A = ( coeff ` F )
	dgrub.2	|- N = ( deg ` F )
Assertion	coeid2	|- ( ( F e. ( Poly ` S ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	|- A = ( coeff ` F )
2		dgrub.2	|- N = ( deg ` F )
3	1 2	coeid	|- ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
4	3	fveq1d	|- ( F e. ( Poly ` S ) -> ( F ` X ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` X ) )
5		oveq1	|- ( z = X -> ( z ^ k ) = ( X ^ k ) )
6	5	oveq2d	|- ( z = X -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( X ^ k ) ) )
7	6	sumeq2sdv	|- ( z = X -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )
8		eqid	|- ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) )
9		sumex	|- sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) e. _V
10	7 8 9	fvmpt	|- ( X e. CC -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )
11	4 10	sylan9eq	|- ( ( F e. ( Poly ` S ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )