Theorem zrhmulg

Description: Value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	zrhval.l	|- L = ( ZRHom ` R )
	zrhval2.m	|- .x. = ( .g ` R )
	zrhval2.1	|- .1. = ( 1r ` R )
Assertion	zrhmulg	|- ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( 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 2 3	zrhval2	|- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )
5	4	fveq1d	|- ( R e. Ring -> ( L ` N ) = ( ( n e. ZZ |-> ( n .x. .1. ) ) ` N ) )
6		oveq1	|- ( n = N -> ( n .x. .1. ) = ( N .x. .1. ) )
7		eqid	|- ( n e. ZZ |-> ( n .x. .1. ) ) = ( n e. ZZ |-> ( n .x. .1. ) )
8		ovex	|- ( N .x. .1. ) e. _V
9	6 7 8	fvmpt	|- ( N e. ZZ -> ( ( n e. ZZ |-> ( n .x. .1. ) ) ` N ) = ( N .x. .1. ) )
10	5 9	sylan9eq	|- ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( N .x. .1. ) )