Theorem coef3

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 ⟶ ℂ )

Proof

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 ⟶ ℂ )