Metamath Proof Explorer


Theorem coef

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

Ref Expression
Hypothesis dgrval.1 𝐴 = ( coeff ‘ 𝐹 )
Assertion coef ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )

Proof

Step Hyp Ref Expression
1 dgrval.1 𝐴 = ( coeff ‘ 𝐹 )
2 1 dgrlem ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
3 2 simpld ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )