zrhval2

Description: Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	zrhval.l	$⊢ L = ℤRHom (R)$
	zrhval2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	zrhval2.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	zrhval2	$⊢ R \in Ring \to L = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$

Step	Hyp	Ref	Expression
1		zrhval.l	$⊢ L = ℤRHom (R)$
2		zrhval2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		zrhval2.1	$⊢ \underset{˙}{1} = 1_{R}$
4	1	zrhval	$⊢ L = ⋃ (ℤ_{ring} RingHom R)$
5		eqid	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1}) = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
6	2 5 3	mulgrhm2	$⊢ R \in Ring \to ℤ_{ring} RingHom R = \{(n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})\}$
7	6	unieqd	$⊢ R \in Ring \to ⋃ (ℤ_{ring} RingHom R) = ⋃ \{(n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})\}$
8		zex	$⊢ ℤ \in V$
9	8	mptex	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1}) \in V$
10	9	unisn	$⊢ ⋃ \{(n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})\} = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
11	7 10	eqtrdi	$⊢ R \in Ring \to ⋃ (ℤ_{ring} RingHom R) = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
12	4 11	eqtrid	$⊢ R \in Ring \to L = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$

Metamath Proof Explorer