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	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		eqid	⊢ 𝐿 = 𝐿
3	1	zrhrhmb	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ↔ 𝐿 = 𝐿 ) )
4	2 3	mpbiri	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )