Metamath Proof Explorer


Theorem oppr0

Description: Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 O=opprR
oppr0.2 0˙=0R
Assertion oppr0 0˙=0O

Proof

Step Hyp Ref Expression
1 opprbas.1 O=opprR
2 oppr0.2 0˙=0R
3 eqid BaseR=BaseR
4 eqid +R=+R
5 3 4 2 grpidval 0˙=ιy|yBaseRxBaseRy+Rx=xx+Ry=x
6 1 3 opprbas BaseR=BaseO
7 1 4 oppradd +R=+O
8 eqid 0O=0O
9 6 7 8 grpidval 0O=ιy|yBaseRxBaseRy+Rx=xx+Ry=x
10 5 9 eqtr4i 0˙=0O