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 = ( 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 ffvelrnda
 |-  ( ( F e. B /\ N e. NN0 ) -> ( A ` N ) e. K )