Theorem coe1f

Description: Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	coe1f.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1f.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1f.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	coe1f	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2		coe1f.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1f.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		coe1f.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5	3 2	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
6		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
7		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8	1 6 7 4	coe1f2	⊢ ( 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) → 𝐴 : ℕ0 ⟶ 𝐾 )
9	5 8	syl	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )