This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑋 ✚ 𝑌 ) = ( 𝑌 + 𝑋 )