Theorem oppradd

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

	Ref	Expression
Hypotheses	opprbas.1	|- O = ( oppR ` R )
	oppradd.2	|- .+ = ( +g ` R )
Assertion	oppradd	|- .+ = ( +g ` O )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	|- O = ( oppR ` R )
2		oppradd.2	|- .+ = ( +g ` R )
3		df-plusg	|- +g = Slot 2
4		2nn	|- 2 e. NN
5		2lt3	|- 2 < 3
6	1 3 4 5	opprlem	|- ( +g ` R ) = ( +g ` O )
7	2 6	eqtri	|- .+ = ( +g ` O )