Metamath Proof Explorer

Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from Z . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 12-Jun-2019)

		Ref	Expression
	Hypothesis	zrhval.l	$⊢ L = ℤRHom (R)$
	Assertion	zrhrhmb	$⊢ R \in Ring \to (F \in (ℤ_{ring} RingHom R) \leftrightarrow F = L)$

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	$⊢ L = ℤRHom (R)$
2		eqid	$⊢ \cdot_{R} = \cdot_{R}$
3		eqid	$⊢ (n \in ℤ ⟼ n \cdot_{R} 1_{R}) = (n \in ℤ ⟼ n \cdot_{R} 1_{R})$
4		eqid	$⊢ 1_{R} = 1_{R}$
5	2 3 4	mulgrhm2	$⊢ R \in Ring \to ℤ_{ring} RingHom R = \{(n \in ℤ ⟼ n \cdot_{R} 1_{R})\}$
6	1 2 4	zrhval2	$⊢ R \in Ring \to L = (n \in ℤ ⟼ n \cdot_{R} 1_{R})$
7	6	sneqd	$⊢ R \in Ring \to \{L\} = \{(n \in ℤ ⟼ n \cdot_{R} 1_{R})\}$
8	5 7	eqtr4d	$⊢ R \in Ring \to ℤ_{ring} RingHom R = \{L\}$
9	8	eleq2d	$⊢ R \in Ring \to (F \in (ℤ_{ring} RingHom R) \leftrightarrow F \in \{L\})$
10	1	fvexi	$⊢ L \in V$
11	10	elsn2	$⊢ F \in \{L\} \leftrightarrow F = L$
12	9 11	bitrdi	$⊢ R \in Ring \to (F \in (ℤ_{ring} RingHom R) \leftrightarrow F = L)$