Definition df-zrh

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 ). (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czrh	⊢ ℤRHom
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		zring	⊢ ℤring
4		crh	⊢ RingHom
5	1	cv	⊢ 𝑟
6	3 5 4	co	⊢ ( ℤring RingHom 𝑟 )
7	6	cuni	⊢ ∪ ( ℤring RingHom 𝑟 )
8	1 2 7	cmpt	⊢ ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )
9	0 8	wceq	⊢ ℤRHom = ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )