# Metamath Proof Explorer

## 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}:{ℕ}_{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}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
3 2 adantr ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge 0\in {S}\right)\to {A}:{ℕ}_{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}↔{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}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}↔{A}:{ℕ}_{0}⟶{S}\right)$
9 3 8 mpbid ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge 0\in {S}\right)\to {A}:{ℕ}_{0}⟶{S}$