Metamath Proof Explorer


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 = coe 1 F
coe1f.b B = Base P
coe1f.p P = Poly 1 R
coe1f.k K = Base R
Assertion coe1fvalcl F B N 0 A N K

Proof

Step Hyp Ref Expression
1 coe1fval.a A = coe 1 F
2 coe1f.b B = Base P
3 coe1f.p P = Poly 1 R
4 coe1f.k K = Base R
5 1 2 3 4 coe1f F B A : 0 K
6 5 ffvelrnda F B N 0 A N K