Theorem coef

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

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

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2	1	dgrlem	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\wedge \exists n\in \mathbb{Z}\forall x\in A^{-1}\left[ℂ\setminus \left\{0\right\}\right]x\le n\right)$$
3	2	simpld	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$