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	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	coe1mul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
	coe1mul.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	coe1mul.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	coe1mul	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)=\left(k\in {\mathbb{N}}_0⟼\underset{x=0}{\overset{k}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(x\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(k-x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1mul.s	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		coe1mul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
3		coe1mul.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		coe1mul.b	$$⊢B={\mathrm{Base}}_Y$$
5		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
6	1 4	ply1bascl	$$⊢F\in B\to F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
7	1 4	ply1bascl	$$⊢G\in B\to G\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
8		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
10		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
11	1 9 2	ply1mulr	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
12	9 10 11	mplmulr	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
13		eqid	$$⊢{\cdot }_{{\mathrm{PwSer}}_1\left(R\right)}={\cdot }_{{\mathrm{PwSer}}_1\left(R\right)}$$
14	8 10 13	psr1mulr	$$⊢{\cdot }_{{\mathrm{PwSer}}_1\left(R\right)}={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
15	12 14	eqtr4i	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{{\mathrm{PwSer}}_1\left(R\right)}$$
16		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
17	8 15 3 16	coe1mul2	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\wedge G\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)=\left(k\in {\mathbb{N}}_0⟼\underset{x=0}{\overset{k}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(x\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(k-x\right)\right)\right)$$
18	5 6 7 17	syl3an	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)=\left(k\in {\mathbb{N}}_0⟼\underset{x=0}{\overset{k}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(x\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(k-x\right)\right)\right)$$