Theorem zrhval2

Description: Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	zrhval.l	|- L = ( ZRHom ` R )
	zrhval2.m	|- .x. = ( .g ` R )
	zrhval2.1	|- .1. = ( 1r ` R )
Assertion	zrhval2	|- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	|- L = ( ZRHom ` R )
2		zrhval2.m	|- .x. = ( .g ` R )
3		zrhval2.1	|- .1. = ( 1r ` R )
4	1	zrhval	|- L = U. ( ZZring RingHom R )
5		eqid	|- ( n e. ZZ |-> ( n .x. .1. ) ) = ( n e. ZZ |-> ( n .x. .1. ) )
6	2 5 3	mulgrhm2	|- ( R e. Ring -> ( ZZring RingHom R ) = { ( n e. ZZ |-> ( n .x. .1. ) ) } )
7	6	unieqd	|- ( R e. Ring -> U. ( ZZring RingHom R ) = U. { ( n e. ZZ |-> ( n .x. .1. ) ) } )
8		zex	|- ZZ e. _V
9	8	mptex	|- ( n e. ZZ |-> ( n .x. .1. ) ) e. _V
10	9	unisn	|- U. { ( n e. ZZ |-> ( n .x. .1. ) ) } = ( n e. ZZ |-> ( n .x. .1. ) )
11	7 10	eqtrdi	|- ( R e. Ring -> U. ( ZZring RingHom R ) = ( n e. ZZ |-> ( n .x. .1. ) ) )
12	4 11	syl5eq	|- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )