Theorem ply1opprmul

Description: Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1opprmul.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	ply1opprmul.s	$$⊢S={opp}_r\left(R\right)$$
	ply1opprmul.z	$$⊢Z={\mathrm{Poly}}_1\left(S\right)$$
	ply1opprmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	ply1opprmul.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
	ply1opprmul.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	ply1opprmul	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=G\underset{\dot{}}{·}F$$

Proof

Step	Hyp	Ref	Expression
1		ply1opprmul.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		ply1opprmul.s	$$⊢S={opp}_r\left(R\right)$$
3		ply1opprmul.z	$$⊢Z={\mathrm{Poly}}_1\left(S\right)$$
4		ply1opprmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
5		ply1opprmul.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
6		ply1opprmul.b	$$⊢B={\mathrm{Base}}_Y$$
7		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
8	1 6	ply1bascl	$$⊢F\in B\to F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
9		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
11	9 10	psr1bascl	$$⊢F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
12	8 11	syl	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
13	1 6	ply1bascl	$$⊢G\in B\to G\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
14	9 10	psr1bascl	$$⊢G\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\to G\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
15	13 14	syl	$$⊢G\in B\to G\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
16		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
17		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}S=1_{𝑜}\mathrm{mPwSer}S$$
18		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
19	1 18 4	ply1mulr	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	18 16 19	mplmulr	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
21		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
22	3 21 5	ply1mulr	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
23	21 17 22	mplmulr	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
24		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
25	16 2 17 20 23 24	psropprmul	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\wedge G\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\right)\to F\underset{\dot{}}{\bullet }G=G\underset{\dot{}}{·}F$$
26	7 12 15 25	syl3an	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=G\underset{\dot{}}{·}F$$