Theorem opprmul

Description: Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Hypotheses	opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	opprval.2	⊢ · = ( .r ‘ 𝑅 )
	opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	opprmulfval.4	⊢ ∙ = ( .r ‘ 𝑂 )
Assertion	opprmul	⊢ ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		opprval.2	⊢ · = ( .r ‘ 𝑅 )
3		opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
4		opprmulfval.4	⊢ ∙ = ( .r ‘ 𝑂 )
5	1 2 3 4	opprmulfval	⊢ ∙ = tpos ·
6	5	oveqi	⊢ ( 𝑋 ∙ 𝑌 ) = ( 𝑋 tpos · 𝑌 )
7		ovtpos	⊢ ( 𝑋 tpos · 𝑌 ) = ( 𝑌 · 𝑋 )
8	6 7	eqtri	⊢ ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 )