This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (r \in V ⟼ ⋃ (ℤ_{ring} RingHom r))$

Detailed syntax breakdown

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