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