Definition df-zrh 19852

Description: Define the unique homomorphism from the integers into a ring. This encodes the usual notation of n = 1r + 1r + ... + 1r for integers (see also df-mulg 17541). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)

Assertion

Ref	Expression
df-zrh	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )

Detailed syntax breakdown of Definition df-zrh

Step	Hyp	Ref	Expression
1		czrh 19848	. 2 class ZRHom
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		zring 19818	. . . . 5 class ℤring
5	2	cv 1482	. . . . 5 class r
6		crh 18712	. . . . 5 class RingHom
7	4, 5, 6	co 6650	. . . 4 class (ℤring RingHom r )
8	7	cuni 4436	. . 3 class U. (ℤring RingHom r )
9	2, 3, 8	cmpt 4729	. 2 class ( r e. _V |-> U. (ℤring RingHom r ) )
10	1, 9	wceq 1483	1 wff ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )

This definition is referenced by:  zrhval  19856