Theorem oppradd

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

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	oppradd.2	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	oppradd	$$⊢\underset{\dot{}}{+}={+}_O$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2		oppradd.2	$$⊢\underset{\dot{}}{+}={+}_R$$
3		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
4		2nn	$$⊢2\in \mathbb{N}$$
5		2lt3	$$⊢2<3$$
6	1 3 4 5	opprlem	$$⊢{+}_R={+}_O$$
7	2 6	eqtri	$$⊢\underset{\dot{}}{+}={+}_O$$