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	$⊢ B = {Base}_{R}$
	opprval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	opprval.3	$⊢ O = {opp}_{r} (R)$
	opprmulfval.4	$⊢ \underset{˙}{∙} = \cdot_{O}$
Assertion	opprmul	$⊢ X \underset{˙}{∙} Y = Y \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		opprval.1	$⊢ B = {Base}_{R}$
2		opprval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		opprval.3	$⊢ O = {opp}_{r} (R)$
4		opprmulfval.4	$⊢ \underset{˙}{∙} = \cdot_{O}$
5	1 2 3 4	opprmulfval	$⊢ \underset{˙}{∙} = tpos \underset{˙}{\cdot}$
6	5	oveqi	$⊢ X \underset{˙}{∙} Y = X tpos \underset{˙}{\cdot} Y$
7		ovtpos	$⊢ X tpos \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
8	6 7	eqtri	$⊢ X \underset{˙}{∙} Y = Y \underset{˙}{\cdot} X$