Theorem coef3

Description: The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
Assertion	coef3	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
3	2	sseli	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
4		0cn	$$⊢0\in ℂ$$
5	1	coef2	$$⊢\left(F\in \mathrm{Poly}\left(ℂ\right)\wedge 0\in ℂ\right)\to A:{\mathbb{N}}_0⟶ℂ$$
6	3 4 5	sylancl	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶ℂ$$