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

Metamath Proof Explorer

Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from ZZ . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypothesis zrhval.l 
|- L = ( ZRHom ` R )
Assertion zrhrhmb 
|- ( R e. Ring -> ( F e. ( ZZring RingHom R ) <-> F = L ) )

Proof

Step Hyp Ref Expression
1 zrhval.l 
 |-  L = ( ZRHom ` R )
2 eqid 
 |-  ( .g ` R ) = ( .g ` R )
3 eqid 
 |-  ( n e. ZZ |-> ( n ( .g ` R ) ( 1r ` R ) ) ) = ( n e. ZZ |-> ( n ( .g ` R ) ( 1r ` R ) ) )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 2 3 4 mulgrhm2 
 |-  ( R e. Ring -> ( ZZring RingHom R ) = { ( n e. ZZ |-> ( n ( .g ` R ) ( 1r ` R ) ) ) } )
6 1 2 4 zrhval2 
 |-  ( R e. Ring -> L = ( n e. ZZ |-> ( n ( .g ` R ) ( 1r ` R ) ) ) )
7 6 sneqd 
 |-  ( R e. Ring -> { L } = { ( n e. ZZ |-> ( n ( .g ` R ) ( 1r ` R ) ) ) } )
8 5 7 eqtr4d 
 |-  ( R e. Ring -> ( ZZring RingHom R ) = { L } )
9 8 eleq2d 
 |-  ( R e. Ring -> ( F e. ( ZZring RingHom R ) <-> F e. { L } ) )
10 1 fvexi 
 |-  L e. _V
11 10 elsn2 
 |-  ( F e. { L } <-> F = L )
12 9 11 bitrdi 
 |-  ( R e. Ring -> ( F e. ( ZZring RingHom R ) <-> F = L ) )