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

Metamath Proof Explorer

Theorem oppradd

Description: Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014) (Proof shortened by AV, 6-Nov-2024)

Step	Hyp	Ref	Expression
1		opprbas.1	$⊢ O = {opp}_{r} (R)$
2		oppradd.2	$⊢ \underset{˙}{+} = +_{R}$
3		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
4		plusgndxnmulrndx	$⊢ +_{ndx} \neq \cdot_{ndx}$
5	1 3 4	opprlem	$⊢ +_{R} = +_{O}$
6	2 5	eqtri	$⊢ \underset{˙}{+} = +_{O}$