Metamath Proof Explorer

Theorem zringinvg

Description: The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Assertion zringinvg 
|- ( A e. ZZ -> -u A = ( ( invg ` ZZring ) ` A ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 negidd 
 |-  ( A e. ZZ -> ( A + -u A ) = 0 )
3 zringgrp 
 |-  ZZring e. Grp
4 id 
 |-  ( A e. ZZ -> A e. ZZ )
5 znegcl 
 |-  ( A e. ZZ -> -u A e. ZZ )
6 zringbas 
 |-  ZZ = ( Base ` ZZring )
7 zringplusg 
 |-  + = ( +g ` ZZring )
8 zring0 
 |-  0 = ( 0g ` ZZring )
9 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
10 6 7 8 9 grpinvid1 
 |-  ( ( ZZring e. Grp /\ A e. ZZ /\ -u A e. ZZ ) -> ( ( ( invg ` ZZring ) ` A ) = -u A <-> ( A + -u A ) = 0 ) )
11 3 4 5 10 mp3an2i 
 |-  ( A e. ZZ -> ( ( ( invg ` ZZring ) ` A ) = -u A <-> ( A + -u A ) = 0 ) )
12 2 11 mpbird 
 |-  ( A e. ZZ -> ( ( invg ` ZZring ) ` A ) = -u A )
13 12 eqcomd 
 |-  ( A e. ZZ -> -u A = ( ( invg ` ZZring ) ` A ) )