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	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	dgrub.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion	coeid2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		dgrub.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3	1 2	coeid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
4	3	fveq1d	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑋 ) )
5		oveq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑘 ) )
6	5	oveq2d	⊢ ( 𝑧 = 𝑋 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
7	6	sumeq2sdv	⊢ ( 𝑧 = 𝑋 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
8		eqid	⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
9		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝑋 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
11	4 10	sylan9eq	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )