Metamath Proof Explorer


Theorem oppradd

Description: Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 O = opp r R
oppradd.2 + ˙ = + R
Assertion oppradd + ˙ = + O

Proof

Step Hyp Ref Expression
1 opprbas.1 O = opp r R
2 oppradd.2 + ˙ = + R
3 df-plusg + 𝑔 = Slot 2
4 2nn 2
5 2lt3 2 < 3
6 1 3 4 5 opprlem + R = + O
7 2 6 eqtri + ˙ = + O