Metamath Proof Explorer


Theorem zrhneg

Description: The canonical homomorphism from the integers to a ring R maps additive inverses to additive inverses. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses zrhneg.1 L = ℤRHom R
zrhneg.2 I = inv g R
zrhneg.3 φ R Ring
zrhneg.4 φ N
Assertion zrhneg φ L N = I L N

Proof

Step Hyp Ref Expression
1 zrhneg.1 L = ℤRHom R
2 zrhneg.2 I = inv g R
3 zrhneg.3 φ R Ring
4 zrhneg.4 φ N
5 zringinvg N N = inv g ring N
6 4 5 syl φ N = inv g ring N
7 6 fveq2d φ L N = L inv g ring N
8 1 zrhrhm R Ring L ring RingHom R
9 rhmghm L ring RingHom R L ring GrpHom R
10 3 8 9 3syl φ L ring GrpHom R
11 zringbas = Base ring
12 eqid inv g ring = inv g ring
13 11 12 2 ghminv L ring GrpHom R N L inv g ring N = I L N
14 10 4 13 syl2anc φ L inv g ring N = I L N
15 7 14 eqtrd φ L N = I L N