Definition df-zrh 20686

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 18682). (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 20682	. 2 class ℤRHom
2		vr	. . 3 setvar 𝑟
3		cvv 3430	. . 3 class V
4		czring 20651	. . . . 5 class ℤring
5	2	cv 1540	. . . . 5 class 𝑟
6		crh 19937	. . . . 5 class RingHom
7	4, 5, 6	co 7268	. . . 4 class (ℤring RingHom 𝑟)
8	7	cuni 4844	. . 3 class ∪ (ℤring RingHom 𝑟)
9	2, 3, 8	cmpt 5161	. 2 class (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
10	1, 9	wceq 1541	1 wff ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))

This definition is referenced by:  zrhval  20690