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={\mathrm{coe}}_1\left(F\right)$$
	coe1f.b	$$⊢B={\mathrm{Base}}_P$$
	coe1f.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1f.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	coe1fvalcl	$$⊢\left(F\in B\wedge N\in {\mathbb{N}}_0\right)\to A\left(N\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		coe1f.b	$$⊢B={\mathrm{Base}}_P$$
3		coe1f.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		coe1f.k	$$⊢K={\mathrm{Base}}_R$$
5	1 2 3 4	coe1f	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$
6	5	ffvelrnda	$$⊢\left(F\in B\wedge N\in {\mathbb{N}}_0\right)\to A\left(N\right)\in K$$