Definition df-zrh 13929

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 13077). (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 13926	. 2 class ZRHom
2		vr	. . 3 setvar r
3		cvv 2752	. . 3 class _V
4		czring 13906	. . . . 5 class ℤring
5	2	cv 1363	. . . . 5 class r
6		crh 13517	. . . . 5 class RingHom
7	4, 5, 6	co 5897	. . . 4 class (ℤring RingHom r )
8	7	cuni 3824	. . 3 class U. (ℤring RingHom r )
9	2, 3, 8	cmpt 4079	. 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:  zrhvalg  13932