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	⊢ ( 𝐴 ∈ ℤ → - 𝐴 = ( ( invg ‘ ℤring ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2	1	negidd	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + - 𝐴 ) = 0 )
3		zringgrp	⊢ ℤring ∈ Grp
4		id	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ )
5		znegcl	⊢ ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
6		zringbas	⊢ ℤ = ( Base ‘ ℤring )
7		zringplusg	⊢ + = ( +g ‘ ℤring )
8		zring0	⊢ 0 = ( 0g ‘ ℤring )
9		eqid	⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
10	6 7 8 9	grpinvid1	⊢ ( ( ℤring ∈ Grp ∧ 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℤ ) → ( ( ( invg ‘ ℤring ) ‘ 𝐴 ) = - 𝐴 ↔ ( 𝐴 + - 𝐴 ) = 0 ) )
11	3 4 5 10	mp3an2i	⊢ ( 𝐴 ∈ ℤ → ( ( ( invg ‘ ℤring ) ‘ 𝐴 ) = - 𝐴 ↔ ( 𝐴 + - 𝐴 ) = 0 ) )
12	2 11	mpbird	⊢ ( 𝐴 ∈ ℤ → ( ( invg ‘ ℤring ) ‘ 𝐴 ) = - 𝐴 )
13	12	eqcomd	⊢ ( 𝐴 ∈ ℤ → - 𝐴 = ( ( invg ‘ ℤring ) ‘ 𝐴 ) )