Metamath Proof Explorer


Theorem rngoaddneg1

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

Ref Expression
Hypotheses ringnegcl.1
|- G = ( 1st ` R )
ringnegcl.2
|- X = ran G
ringnegcl.3
|- N = ( inv ` G )
ringaddneg.4
|- Z = ( GId ` G )
Assertion rngoaddneg1
|- ( ( R e. RingOps /\ A e. X ) -> ( A G ( N ` A ) ) = Z )

Proof

Step Hyp Ref Expression
1 ringnegcl.1
 |-  G = ( 1st ` R )
2 ringnegcl.2
 |-  X = ran G
3 ringnegcl.3
 |-  N = ( inv ` G )
4 ringaddneg.4
 |-  Z = ( GId ` G )
5 1 rngogrpo
 |-  ( R e. RingOps -> G e. GrpOp )
6 2 4 3 grporinv
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A G ( N ` A ) ) = Z )
7 5 6 sylan
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A G ( N ` A ) ) = Z )