This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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