This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝑂 = ( opp_r ‘ 𝑅 )
	opprmulfval.4	⊢ ∙ = ( ._r ‘ 𝑂 )
Assertion	opprmul	⊢ ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 )

Proof

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