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	$$⊢\mathrm{\mathbb{Z}RHom}=\left(r\in \mathrm{V}⟼\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czrh	$$class\mathrm{\mathbb{Z}RHom}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		czring	$$class{\mathbb{Z}}_{\mathrm{ring}}$$
4		crh	$$class\mathrm{RingHom}$$
5	1	cv	$$setvarr$$
6	3 5 4	co	$$class\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)$$
7	6	cuni	$$class\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)$$
8	1 2 7	cmpt	$$class\left(r\in \mathrm{V}⟼\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)\right)$$
9	0 8	wceq	$$wff\mathrm{\mathbb{Z}RHom}=\left(r\in \mathrm{V}⟼\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)\right)$$