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 ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
coe1f.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1f.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1f.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion coe1fvalcl ( ( 𝐹 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑁 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 coe1fval.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2 coe1f.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 coe1f.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 coe1f.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 1 2 3 4 coe1f ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )
6 5 ffvelcdmda ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑁 ) ∈ 𝐾 )