# Metamath Proof Explorer

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

### Proof

Step Hyp Ref Expression
1 dgrub.1 ${⊢}{A}=\mathrm{coeff}\left({F}\right)$
2 dgrub.2 ${⊢}{N}=\mathrm{deg}\left({F}\right)$
3 elply2 ${⊢}{F}\in \mathrm{Poly}\left({S}\right)↔\left({S}\subseteq ℂ\wedge \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}\left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)$
4 3 simprbi ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}\left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)$
5 simpll ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {F}\in \mathrm{Poly}\left({S}\right)$
6 simplrl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {n}\in {ℕ}_{0}$
7 simplrr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
8 simprl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}$
9 simprr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)$
10 fveq2 ${⊢}{m}={k}\to {a}\left({m}\right)={a}\left({k}\right)$
11 oveq2 ${⊢}{m}={k}\to {{x}}^{{m}}={{x}}^{{k}}$
12 10 11 oveq12d ${⊢}{m}={k}\to {a}\left({m}\right){{x}}^{{m}}={a}\left({k}\right){{x}}^{{k}}$
13 12 cbvsumv ${⊢}\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}=\sum _{{k}=0}^{{n}}{a}\left({k}\right){{x}}^{{k}}$
14 oveq1 ${⊢}{x}={z}\to {{x}}^{{k}}={{z}}^{{k}}$
15 14 oveq2d ${⊢}{x}={z}\to {a}\left({k}\right){{x}}^{{k}}={a}\left({k}\right){{z}}^{{k}}$
16 15 sumeq2sdv ${⊢}{x}={z}\to \sum _{{k}=0}^{{n}}{a}\left({k}\right){{x}}^{{k}}=\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}$
17 13 16 syl5eq ${⊢}{x}={z}\to \sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}=\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}$
18 17 cbvmptv ${⊢}\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
19 9 18 eqtrdi ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
20 1 2 5 6 7 8 19 coeidlem ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge \left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)$
21 20 ex ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\to \left(\left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\right)$
22 21 rexlimdvva ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}\left({a}\left[{ℤ}_{\ge \left({n}+1\right)}\right]=\left\{0\right\}\wedge {F}=\left({x}\in ℂ⟼\sum _{{m}=0}^{{n}}{a}\left({m}\right){{x}}^{{m}}\right)\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\right)$
23 4 22 mpd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)$