Theorem oppradd

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

	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		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
4		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
5	1 3 4	opprlem	$$⊢{+}_R={+}_O$$
6	2 5	eqtri	$$⊢\underset{\dot{}}{+}={+}_O$$