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 = ( ZRHom ` R )
	zrhneg.2	|- I = ( invg ` R )
	zrhneg.3	|- ( ph -> R e. Ring )
	zrhneg.4	|- ( ph -> N e. ZZ )
Assertion	zrhneg	|- ( ph -> ( L ` -u N ) = ( I ` ( L ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		zrhneg.1	|- L = ( ZRHom ` R )
2		zrhneg.2	|- I = ( invg ` R )
3		zrhneg.3	|- ( ph -> R e. Ring )
4		zrhneg.4	|- ( ph -> N e. ZZ )
5		zringinvg	|- ( N e. ZZ -> -u N = ( ( invg ` ZZring ) ` N ) )
6	4 5	syl	|- ( ph -> -u N = ( ( invg ` ZZring ) ` N ) )
7	6	fveq2d	|- ( ph -> ( L ` -u N ) = ( L ` ( ( invg ` ZZring ) ` N ) ) )
8	1	zrhrhm	|- ( R e. Ring -> L e. ( ZZring RingHom R ) )
9		rhmghm	|- ( L e. ( ZZring RingHom R ) -> L e. ( ZZring GrpHom R ) )
10	3 8 9	3syl	|- ( ph -> L e. ( ZZring GrpHom R ) )
11		zringbas	|- ZZ = ( Base ` ZZring )
12		eqid	|- ( invg ` ZZring ) = ( invg ` ZZring )
13	11 12 2	ghminv	|- ( ( L e. ( ZZring GrpHom R ) /\ N e. ZZ ) -> ( L ` ( ( invg ` ZZring ) ` N ) ) = ( I ` ( L ` N ) ) )
14	10 4 13	syl2anc	|- ( ph -> ( L ` ( ( invg ` ZZring ) ` N ) ) = ( I ` ( L ` N ) ) )
15	7 14	eqtrd	|- ( ph -> ( L ` -u N ) = ( I ` ( L ` N ) ) )