Definition df-zrh 21514

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 19086). (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 21510	. 2 class ℤRHom
2		vr	. . 3 setvar 𝑟
3		cvv 3480	. . 3 class V
4		czring 21457	. . . . 5 class ℤring
5	2	cv 1539	. . . . 5 class 𝑟
6		crh 20469	. . . . 5 class RingHom
7	4, 5, 6	co 7431	. . . 4 class (ℤring RingHom 𝑟)
8	7	cuni 4907	. . 3 class ∪ (ℤring RingHom 𝑟)
9	2, 3, 8	cmpt 5225	. 2 class (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
10	1, 9	wceq 1540	1 wff ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))

This definition is referenced by:  zrhval  21518