Theorem coeid

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	coeid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		dgrub.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3		elply2	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) )
5		simpll	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6		simplrl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝑛 ∈ ℕ0 )
7		simplrr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
8		simprl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
9		simprr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) )
10		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑎 ‘ 𝑚 ) = ( 𝑎 ‘ 𝑘 ) )
11		oveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑥 ↑ 𝑚 ) = ( 𝑥 ↑ 𝑘 ) )
12	10 11	oveq12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
13	12	cbvsumv	⊢ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) )
14		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ↑ 𝑘 ) = ( 𝑧 ↑ 𝑘 ) )
15	14	oveq2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
16	15	sumeq2sdv	⊢ ( 𝑥 = 𝑧 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
17	13 16	eqtrid	⊢ ( 𝑥 = 𝑧 → Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
18	17	cbvmptv	⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
19	9 18	eqtrdi	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
20	1 2 5 6 7 8 19	coeidlem	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
21	20	ex	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
22	21	rexlimdvva	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
23	4 22	mpd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )