This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coef

Description: The domain and codomain 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 } ) )