Theorem coe1fvalcl

Description: A coefficient of a univariate polynomial over a class/ring is an element of this class/ring. (Contributed by AV, 9-Oct-2019)

	Ref	Expression
Hypotheses	coe1fval.a	|- A = ( coe1 ` F )
	coe1f.b	|- B = ( Base ` P )
	coe1f.p	|- P = ( Poly1 ` R )
	coe1f.k	|- K = ( Base ` R )
Assertion	coe1fvalcl	|- ( ( F e. B /\ N e. NN0 ) -> ( A ` N ) e. K )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	|- A = ( coe1 ` F )
2		coe1f.b	|- B = ( Base ` P )
3		coe1f.p	|- P = ( Poly1 ` R )
4		coe1f.k	|- K = ( Base ` R )
5	1 2 3 4	coe1f	|- ( F e. B -> A : NN0 --> K )
6	5	ffvelcdmda	|- ( ( F e. B /\ N e. NN0 ) -> ( A ` N ) e. K )