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 ‘ 𝑅 )
	oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
	oppgplusfval.4	⊢ ✚ = ( +g ‘ 𝑂 )
Assertion	oppgplus	⊢ ( 𝑋 ✚ 𝑌 ) = ( 𝑌 + 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	⊢ + = ( +g ‘ 𝑅 )
2		oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
3		oppgplusfval.4	⊢ ✚ = ( +g ‘ 𝑂 )
4	1 2 3	oppgplusfval	⊢ ✚ = tpos +
5	4	oveqi	⊢ ( 𝑋 ✚ 𝑌 ) = ( 𝑋 tpos + 𝑌 )
6		ovtpos	⊢ ( 𝑋 tpos + 𝑌 ) = ( 𝑌 + 𝑋 )
7	5 6	eqtri	⊢ ( 𝑋 ✚ 𝑌 ) = ( 𝑌 + 𝑋 )