Theorem zrhval2

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

	Ref	Expression
Hypotheses	zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	zrhval2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	zrhval2.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	zrhval2	$$⊢R\in \mathrm{Ring}\to L=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		zrhval2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		zrhval2.1	$$⊢\underset{\dot{}}{1}=1_R$$
4	1	zrhval	$$⊢L=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
5		eqid	$$⊢\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
6	2 5 3	mulgrhm2	$$⊢R\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R=\left\{\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right\}$$
7	6	unieqd	$$⊢R\in \mathrm{Ring}\to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)=\bigcup \left\{\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right\}$$
8		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
9	8	mptex	$$⊢\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\in \mathrm{V}$$
10	9	unisn	$$⊢\bigcup \left\{\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right\}=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
11	7 10	syl6eq	$$⊢R\in \mathrm{Ring}\to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
12	4 11	syl5eq	$$⊢R\in \mathrm{Ring}\to L=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$