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 ) → ( 𝐴 ‘ 𝑁 ) ∈ 𝐾 )