Definition df-zrh 14102

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

Assertion

Ref	Expression
df-zrh	⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))

Detailed syntax breakdown of Definition df-zrh

Step	Hyp	Ref	Expression
1		czrh 14099	. 2 class ℤRHom
2		vr	. . 3 setvar 𝑟
3		cvv 2760	. . 3 class V
4		czring 14078	. . . . 5 class ℤring
5	2	cv 1363	. . . . 5 class 𝑟
6		crh 13646	. . . . 5 class RingHom
7	4, 5, 6	co 5918	. . . 4 class (ℤring RingHom 𝑟)
8	7	cuni 3835	. . 3 class ∪ (ℤring RingHom 𝑟)
9	2, 3, 8	cmpt 4090	. 2 class (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
10	1, 9	wceq 1364	1 wff ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))

This definition is referenced by:  zrhval  14105  zrhvalg  14106