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

Ref | Expression | ||
---|---|---|---|

Hypothesis | dgrval.1 | ⊢ 𝐴 = ( coeff ‘ 𝐹 ) | |

Assertion | coef3 | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ_{0} ⟶ ℂ ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | dgrval.1 | ⊢ 𝐴 = ( coeff ‘ 𝐹 ) | |

2 | plyssc | ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) | |

3 | 2 | sseli | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) ) |

4 | 0cn | ⊢ 0 ∈ ℂ | |

5 | 1 | coef2 | ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 0 ∈ ℂ ) → 𝐴 : ℕ_{0} ⟶ ℂ ) |

6 | 3 4 5 | sylancl | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ_{0} ⟶ ℂ ) |