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	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhneg.2	⊢ 𝐼 = ( invg ‘ 𝑅 )
	zrhneg.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	zrhneg.4	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	zrhneg	⊢ ( 𝜑 → ( 𝐿 ‘ - 𝑁 ) = ( 𝐼 ‘ ( 𝐿 ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zrhneg.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		zrhneg.2	⊢ 𝐼 = ( invg ‘ 𝑅 )
3		zrhneg.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		zrhneg.4	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		zringinvg	⊢ ( 𝑁 ∈ ℤ → - 𝑁 = ( ( invg ‘ ℤring ) ‘ 𝑁 ) )
6	4 5	syl	⊢ ( 𝜑 → - 𝑁 = ( ( invg ‘ ℤring ) ‘ 𝑁 ) )
7	6	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ - 𝑁 ) = ( 𝐿 ‘ ( ( invg ‘ ℤring ) ‘ 𝑁 ) ) )
8	1	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
9		rhmghm	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
10	3 8 9	3syl	⊢ ( 𝜑 → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
11		zringbas	⊢ ℤ = ( Base ‘ ℤring )
12		eqid	⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
13	11 12 2	ghminv	⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ ( ( invg ‘ ℤring ) ‘ 𝑁 ) ) = ( 𝐼 ‘ ( 𝐿 ‘ 𝑁 ) ) )
14	10 4 13	syl2anc	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( invg ‘ ℤring ) ‘ 𝑁 ) ) = ( 𝐼 ‘ ( 𝐿 ‘ 𝑁 ) ) )
15	7 14	eqtrd	⊢ ( 𝜑 → ( 𝐿 ‘ - 𝑁 ) = ( 𝐼 ‘ ( 𝐿 ‘ 𝑁 ) ) )