This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ) )