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 ) |
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 ) |