Theorem zrhrhm

Description: The ZRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypothesis	zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
Assertion	zrhrhm	$$⊢R\in \mathrm{Ring}\to L\in \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		eqid	$$⊢L=L$$
3	1	zrhrhmb	$$⊢R\in \mathrm{Ring}\to \left(L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\leftrightarrow L=L\right)$$
4	2 3	mpbiri	$$⊢R\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$