Theorem coe1mul

Description: The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1mul.s	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	coe1mul.t	⊢ ∙ = ( .r ‘ 𝑌 )
	coe1mul.u	⊢ · = ( .r ‘ 𝑅 )
	coe1mul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	coe1mul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe1 ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1mul.s	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		coe1mul.t	⊢ ∙ = ( .r ‘ 𝑌 )
3		coe1mul.u	⊢ · = ( .r ‘ 𝑅 )
4		coe1mul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
6	1 4	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
7	1 4	ply1bascl	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
8		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
9		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
10		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
11	1 9 2	ply1mulr	⊢ ∙ = ( .r ‘ ( 1o mPoly 𝑅 ) )
12	9 10 11	mplmulr	⊢ ∙ = ( .r ‘ ( 1o mPwSer 𝑅 ) )
13		eqid	⊢ ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ ( PwSer1 ‘ 𝑅 ) )
14	8 10 13	psr1mulr	⊢ ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
15	12 14	eqtr4i	⊢ ∙ = ( .r ‘ ( PwSer1 ‘ 𝑅 ) )
16		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
17	8 15 3 16	coe1mul2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) ∧ 𝐺 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) ) → ( coe1 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe1 ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )
18	5 6 7 17	syl3an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe1 ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )