Theorem coef3

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

	Ref	Expression
Hypothesis	dgrval.1	|- A = ( coeff ` F )
Assertion	coef3	|- ( F e. ( Poly ` S ) -> A : NN0 --> CC )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	|- A = ( coeff ` F )
2		plyssc	|- ( Poly ` S ) C_ ( Poly ` CC )
3	2	sseli	|- ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
4		0cn	|- 0 e. CC
5	1	coef2	|- ( ( F e. ( Poly ` CC ) /\ 0 e. CC ) -> A : NN0 --> CC )
6	3 4 5	sylancl	|- ( F e. ( Poly ` S ) -> A : NN0 --> CC )