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