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

Metamath Proof Explorer

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