Theorem coe1fval2

Description: Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	coe1f.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1f.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1fval2.g	⊢ 𝐺 = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
Assertion	coe1fval2	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2		coe1f.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1f.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		coe1fval2.g	⊢ 𝐺 = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
5	3 2	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
6		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
7		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8	1 6 7 4	coe1fval3	⊢ ( 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) → 𝐴 = ( 𝐹 ∘ 𝐺 ) )
9	5 8	syl	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ 𝐺 ) )