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