Theorem oppgplus

Description: Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Fan Zheng, 26-Jun-2016)

	Ref	Expression
Hypotheses	oppgval.2	|- .+ = ( +g ` R )
	oppgval.3	|- O = ( oppG ` R )
	oppgplusfval.4	|- .+b = ( +g ` O )
Assertion	oppgplus	|- ( X .+b Y ) = ( Y .+ X )

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	|- .+ = ( +g ` R )
2		oppgval.3	|- O = ( oppG ` R )
3		oppgplusfval.4	|- .+b = ( +g ` O )
4	1 2 3	oppgplusfval	|- .+b = tpos .+
5	4	oveqi	|- ( X .+b Y ) = ( X tpos .+ Y )
6		ovtpos	|- ( X tpos .+ Y ) = ( Y .+ X )
7	5 6	eqtri	|- ( X .+b Y ) = ( Y .+ X )