Definition df-zrh 14248

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 13328). (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 14245	. 2 class ZRHom
2		vr	. . 3 setvar r
3		cvv 2763	. . 3 class _V
4		czring 14224	. . . . 5 class ℤring
5	2	cv 1363	. . . . 5 class r
6		crh 13784	. . . . 5 class RingHom
7	4, 5, 6	co 5925	. . . 4 class (ℤring RingHom r )
8	7	cuni 3840	. . 3 class U. (ℤring RingHom r )
9	2, 3, 8	cmpt 4095	. 2 class ( r e. _V |-> U. (ℤring RingHom r ) )
10	1, 9	wceq 1364	1 wff ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )

This definition is referenced by:  zrhval  14251  zrhvalg  14252