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 ` 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 )