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	$$⊢\underset{\dot{}}{+}={+}_R$$
	oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
	oppgplusfval.4	$$⊢\underset{\dot{}}{✚}={+}_O$$
Assertion	oppgplus	$$⊢X\underset{\dot{}}{✚}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	$$⊢\underset{\dot{}}{+}={+}_R$$
2		oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
3		oppgplusfval.4	$$⊢\underset{\dot{}}{✚}={+}_O$$
4	1 2 3	oppgplusfval	$$⊢\underset{\dot{}}{✚}=tpos\underset{\dot{}}{+}$$
5	4	oveqi	$$⊢X\underset{\dot{}}{✚}Y=Xtpos\underset{\dot{}}{+}Y$$
6		ovtpos	$$⊢Xtpos\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
7	5 6	eqtri	$$⊢X\underset{\dot{}}{✚}Y=Y\underset{\dot{}}{+}X$$