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=\mathrm{coeff}\left(F\right)$$
	dgrub.2	$$⊢N=\mathrm{deg}\left(F\right)$$
Assertion	coeid2	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge X\in ℂ\right)\to F\left(X\right)=\sum _{k=0}^{N}A\left(k\right)X^k$$

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		dgrub.2	$$⊢N=\mathrm{deg}\left(F\right)$$
3	1 2	coeid	$$⊢F\in \mathrm{Poly}\left(S\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
4	3	fveq1d	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\left(X\right)=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\left(X\right)$$
5		oveq1	$$⊢z=X\to z^k=X^k$$
6	5	oveq2d	$$⊢z=X\to A\left(k\right)z^k=A\left(k\right)X^k$$
7	6	sumeq2sdv	$$⊢z=X\to \sum _{k=0}^{N}A\left(k\right)z^k=\sum _{k=0}^{N}A\left(k\right)X^k$$
8		eqid	$$⊢\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
9		sumex	$$⊢\sum _{k=0}^{N}A\left(k\right)X^k\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢X\in ℂ\to \left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\left(X\right)=\sum _{k=0}^{N}A\left(k\right)X^k$$
11	4 10	sylan9eq	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge X\in ℂ\right)\to F\left(X\right)=\sum _{k=0}^{N}A\left(k\right)X^k$$