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

Metamath Proof Explorer

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 eqtrid 
 |-  ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )