Metamath Proof Explorer


Theorem rngoaddneg2

Description: Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses ringnegcl.1 G = 1 st R
ringnegcl.2 X = ran G
ringnegcl.3 N = inv G
ringaddneg.4 Z = GId G
Assertion rngoaddneg2 R RingOps A X N A G A = Z

Proof

Step Hyp Ref Expression
1 ringnegcl.1 G = 1 st R
2 ringnegcl.2 X = ran G
3 ringnegcl.3 N = inv G
4 ringaddneg.4 Z = GId G
5 1 rngogrpo R RingOps G GrpOp
6 2 4 3 grpolinv G GrpOp A X N A G A = Z
7 5 6 sylan R RingOps A X N A G A = Z