Theorem oppraddOLD

Description: Obsolete proof of opprbas as of 6-Nov-2024. Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	oppradd.2	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	oppraddOLD	$$⊢\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	opprlemOLD	$$⊢{+}_R={+}_O$$
7	2 6	eqtri	$$⊢\underset{\dot{}}{+}={+}_O$$