Theorem zrhval

Description: Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypothesis	zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
Assertion	zrhval	$$⊢L=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		oveq2	$$⊢r=R\to {\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r={\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R$$
3	2	unieqd	$$⊢r=R\to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
4		df-zrh	$$⊢\mathrm{\mathbb{Z}RHom}=\left(r\in \mathrm{V}⟼\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}r\right)\right)$$
5		ovex	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\in \mathrm{V}$$
6	5	uniex	$$⊢\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\in \mathrm{V}$$
7	3 4 6	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{\mathbb{Z}RHom}\left(R\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
8		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{\mathbb{Z}RHom}\left(R\right)=\varnothing$$
9		dfrhm2	$$⊢\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼\left(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\right)$$
10	9	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{RingHom}$$
11	10	ovprc2	$$⊢\neg R\in \mathrm{V}\to {\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R=\varnothing$$
12	11	unieqd	$$⊢\neg R\in \mathrm{V}\to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)=\bigcup \varnothing$$
13		uni0	$$⊢\bigcup \varnothing =\varnothing$$
14	12 13	eqtrdi	$$⊢\neg R\in \mathrm{V}\to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)=\varnothing$$
15	8 14	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \mathrm{\mathbb{Z}RHom}\left(R\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
16	7 15	pm2.61i	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
17	1 16	eqtri	$$⊢L=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$