Definition df-zrh 14409

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 13489). (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 14406	. 2 class ZRHom
2		vr	. . 3 setvar r
3		cvv 2772	. . 3 class _V
4		czring 14385	. . . . 5 class ℤring
5	2	cv 1372	. . . . 5 class r
6		crh 13945	. . . . 5 class RingHom
7	4, 5, 6	co 5946	. . . 4 class (ℤring RingHom r )
8	7	cuni 3850	. . 3 class U. (ℤring RingHom r )
9	2, 3, 8	cmpt 4106	. 2 class ( r e. _V |-> U. (ℤring RingHom r ) )
10	1, 9	wceq 1373	1 wff ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )

This definition is referenced by:  zrhval  14412  zrhvalg  14413