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=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	zrhneg.2	$$⊢I={inv}_g\left(R\right)$$
	zrhneg.3	$$⊢\phi \to R\in \mathrm{Ring}$$
	zrhneg.4	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	zrhneg	$$⊢\phi \to L\left(-N\right)=I\left(L\left(N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrhneg.1	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		zrhneg.2	$$⊢I={inv}_g\left(R\right)$$
3		zrhneg.3	$$⊢\phi \to R\in \mathrm{Ring}$$
4		zrhneg.4	$$⊢\phi \to N\in \mathbb{Z}$$
5		zringinvg	$$⊢N\in \mathbb{Z}\to -N={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(N\right)$$
6	4 5	syl	$$⊢\phi \to -N={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(N\right)$$
7	6	fveq2d	$$⊢\phi \to L\left(-N\right)=L\left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(N\right)\right)$$
8	1	zrhrhm	$$⊢R\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
9		rhmghm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)$$
10	3 8 9	3syl	$$⊢\phi \to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)$$
11		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
12		eqid	$$⊢{inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
13	11 12 2	ghminv	$$⊢\left(L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)\wedge N\in \mathbb{Z}\right)\to L\left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(N\right)\right)=I\left(L\left(N\right)\right)$$
14	10 4 13	syl2anc	$$⊢\phi \to L\left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(N\right)\right)=I\left(L\left(N\right)\right)$$
15	7 14	eqtrd	$$⊢\phi \to L\left(-N\right)=I\left(L\left(N\right)\right)$$