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 = {Poly}_{1} (R)$
	ply1opprmul.s	$⊢ S = {opp}_{r} (R)$
	ply1opprmul.z	$⊢ Z = {Poly}_{1} (S)$
	ply1opprmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	ply1opprmul.u	$⊢ \underset{˙}{∙} = \cdot_{Z}$
	ply1opprmul.b	$⊢ B = {Base}_{Y}$
Assertion	ply1opprmul	$⊢ (R \in Ring \land F \in B \land G \in B) \to F \underset{˙}{∙} G = G \underset{˙}{\cdot} F$

Proof

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

Metamath Proof Explorer

Theorem ply1opprmul

Proof