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	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
	ply1opprmul.s	⊢ 𝑆 = ( opp_r ‘ 𝑅 )
	ply1opprmul.z	⊢ 𝑍 = ( Poly₁ ‘ 𝑆 )
	ply1opprmul.t	⊢ · = ( ._r ‘ 𝑌 )
	ply1opprmul.u	⊢ ∙ = ( ._r ‘ 𝑍 )
	ply1opprmul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	ply1opprmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1opprmul.y	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
2		ply1opprmul.s	⊢ 𝑆 = ( opp_r ‘ 𝑅 )
3		ply1opprmul.z	⊢ 𝑍 = ( Poly₁ ‘ 𝑆 )
4		ply1opprmul.t	⊢ · = ( ._r ‘ 𝑌 )
5		ply1opprmul.u	⊢ ∙ = ( ._r ‘ 𝑍 )
6		ply1opprmul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
7		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
8	1 6	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) )
9		eqid	⊢ ( PwSer₁ ‘ 𝑅 ) = ( PwSer₁ ‘ 𝑅 )
10		eqid	⊢ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( Base ‘ ( PwSer₁ ‘ 𝑅 ) )
11	9 10	psr1bascl	⊢ ( 𝐹 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) → 𝐹 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) )
12	8 11	syl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) )
13	1 6	ply1bascl	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) )
14	9 10	psr1bascl	⊢ ( 𝐺 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) → 𝐺 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) )
15	13 14	syl	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) )
16		eqid	⊢ ( 1_o mPwSer 𝑅 ) = ( 1_o mPwSer 𝑅 )
17		eqid	⊢ ( 1_o mPwSer 𝑆 ) = ( 1_o mPwSer 𝑆 )
18		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
19	1 18 4	ply1mulr	⊢ · = ( ._r ‘ ( 1_o mPoly 𝑅 ) )
20	18 16 19	mplmulr	⊢ · = ( ._r ‘ ( 1_o mPwSer 𝑅 ) )
21		eqid	⊢ ( 1_o mPoly 𝑆 ) = ( 1_o mPoly 𝑆 )
22	3 21 5	ply1mulr	⊢ ∙ = ( ._r ‘ ( 1_o mPoly 𝑆 ) )
23	21 17 22	mplmulr	⊢ ∙ = ( ._r ‘ ( 1_o mPwSer 𝑆 ) )
24		eqid	⊢ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) = ( Base ‘ ( 1_o mPwSer 𝑅 ) )
25	16 2 17 20 23 24	psropprmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) ∧ 𝐺 ∈ ( Base ‘ ( 1_o mPwSer 𝑅 ) ) ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )
26	7 12 15 25	syl3an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )

Metamath Proof Explorer

Theorem ply1opprmul

Proof