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

Metamath Proof Explorer

Theorem oppgplus

Description: Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Fan Zheng, 26-Jun-2016)

Step	Hyp	Ref	Expression
1		oppgval.2	$⊢ \underset{˙}{+} = +_{R}$
2		oppgval.3	$⊢ O = {opp}_{𝑔} (R)$
3		oppgplusfval.4	$⊢ \underset{˙}{✚} = +_{O}$
4	1 2 3	oppgplusfval	$⊢ \underset{˙}{✚} = tpos \underset{˙}{+}$
5	4	oveqi	$⊢ X \underset{˙}{✚} Y = X tpos \underset{˙}{+} Y$
6		ovtpos	$⊢ X tpos \underset{˙}{+} Y = Y \underset{˙}{+} X$
7	5 6	eqtri	$⊢ X \underset{˙}{✚} Y = Y \underset{˙}{+} X$