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
|- L = ( ZRHom ` R )
Assertion zrhrhm
|- ( R e. Ring -> L e. ( ZZring RingHom R ) )

Proof

Step Hyp Ref Expression
1 zrhval.l
 |-  L = ( ZRHom ` R )
2 eqid
 |-  L = L
3 1 zrhrhmb
 |-  ( R e. Ring -> ( L e. ( ZZring RingHom R ) <-> L = L ) )
4 2 3 mpbiri
 |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )