Theorem coef2

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	coef2	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to A:{\mathbb{N}}_0⟶S$$

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2	1	coef	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
3	2	adantr	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
4		simpr	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to 0\in S$$
5	4	snssd	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to \left\{0\right\}\subseteq S$$
6		ssequn2	$$⊢\left\{0\right\}\subseteq S\leftrightarrow S\cup \left\{0\right\}=S$$
7	5 6	sylib	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to S\cup \left\{0\right\}=S$$
8	7	feq3d	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to \left(A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\leftrightarrow A:{\mathbb{N}}_0⟶S\right)$$
9	3 8	mpbid	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to A:{\mathbb{N}}_0⟶S$$