Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	coelem	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(\mathrm{coeff}\left(F\right)\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge \exists n\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coeval	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{coeff}\left(F\right)=\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)$$
2		coeeu	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
3		riotacl2	$$⊢\exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\to \left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\in \left\{a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right\}$$
4	2 3	syl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\in \left\{a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right\}$$
5	1 4	eqeltrd	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{coeff}\left(F\right)\in \left\{a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right\}$$
6		imaeq1	$$⊢a=\mathrm{coeff}\left(F\right)\to a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]$$
7	6	eqeq1d	$$⊢a=\mathrm{coeff}\left(F\right)\to \left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\leftrightarrow \mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\right)$$
8		fveq1	$$⊢a=\mathrm{coeff}\left(F\right)\to a\left(k\right)=\mathrm{coeff}\left(F\right)\left(k\right)$$
9	8	oveq1d	$$⊢a=\mathrm{coeff}\left(F\right)\to a\left(k\right)z^k=\mathrm{coeff}\left(F\right)\left(k\right)z^k$$
10	9	sumeq2sdv	$$⊢a=\mathrm{coeff}\left(F\right)\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k$$
11	10	mpteq2dv	$$⊢a=\mathrm{coeff}\left(F\right)\to \left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)$$
12	11	eqeq2d	$$⊢a=\mathrm{coeff}\left(F\right)\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)$$
13	7 12	anbi12d	$$⊢a=\mathrm{coeff}\left(F\right)\to \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)\right)$$
14	13	rexbidv	$$⊢a=\mathrm{coeff}\left(F\right)\to \left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)\right)$$
15	14	elrab	$$⊢\mathrm{coeff}\left(F\right)\in \left\{a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right\}\leftrightarrow \left(\mathrm{coeff}\left(F\right)\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge \exists n\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)\right)$$
16	5 15	sylib	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(\mathrm{coeff}\left(F\right)\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge \exists n\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^n\mathrm{coeff}\left(F\right)\left(k\right)z^k\right)\right)\right)$$