Theorem coeval

Description: Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
2	1	sseli	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
3		eqeq1	$$⊢f=F\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}a\left(k\right)z^k\right)\right)$$
4	3	anbi2d	$$⊢f=F\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(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	4	rexbidv	$$⊢f=F\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(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	5	riotabidv	$$⊢f=F\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)=\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)$$
7		df-coe	$$⊢\mathrm{coeff}=\left(f\in \mathrm{Poly}\left(ℂ\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)\right)$$
8		riotaex	$$⊢\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 \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢F\in \mathrm{Poly}\left(ℂ\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)$$
10	2 9	syl	$$⊢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)$$