Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from Z . (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 ) )