Definition df-zrh 21824

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 19293). (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 21820	. 2 class ℤRHom
2		vr	. . 3 setvar 𝑟
3		cvv 3454	. . 3 class V
4		czring 21767	. . . . 5 class ℤring
5	2	cv 1568	. . . . 5 class 𝑟
6		crh 20714	. . . . 5 class RingHom
7	4, 5, 6	co 7430	. . . 4 class (ℤring RingHom 𝑟)
8	7	cuni 4870	. . 3 class ∪ (ℤring RingHom 𝑟)
9	2, 3, 8	cmpt 5189	. 2 class (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
10	1, 9	wceq 1569	1 wff ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))

This definition is used by:  zrhval  21828