This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ F ∈ B ∧ N ∈ ℕ 0 → A ⁡ N ∈ K