Metamath Proof Explorer

Theorem zrhval

Description: Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypothesis zrhval.l 
|- L = ( ZRHom ` R )
Assertion zrhval 
|- L = U. ( ZZring RingHom R )

Proof

Step Hyp Ref Expression
1 zrhval.l 
 |-  L = ( ZRHom ` R )
2 oveq2 
 |-  ( r = R -> ( ZZring RingHom r ) = ( ZZring RingHom R ) )
3 2 unieqd 
 |-  ( r = R -> U. ( ZZring RingHom r ) = U. ( ZZring RingHom R ) )
4 df-zrh 
 |-  ZRHom = ( r e. _V |-> U. ( ZZring RingHom r ) )
5 ovex 
 |-  ( ZZring RingHom R ) e. _V
6 5 uniex 
 |-  U. ( ZZring RingHom R ) e. _V
7 3 4 6 fvmpt 
 |-  ( R e. _V -> ( ZRHom ` R ) = U. ( ZZring RingHom R ) )
8 fvprc 
 |-  ( -. R e. _V -> ( ZRHom ` R ) = (/) )
9 dfrhm2 
 |-  RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) )
10 9 reldmmpo 
 |-  Rel dom RingHom
11 10 ovprc2 
 |-  ( -. R e. _V -> ( ZZring RingHom R ) = (/) )
12 11 unieqd 
 |-  ( -. R e. _V -> U. ( ZZring RingHom R ) = U. (/) )
13 uni0 
 |-  U. (/) = (/)
14 12 13 eqtrdi 
 |-  ( -. R e. _V -> U. ( ZZring RingHom R ) = (/) )
15 8 14 eqtr4d 
 |-  ( -. R e. _V -> ( ZRHom ` R ) = U. ( ZZring RingHom R ) )
16 7 15 pm2.61i 
 |-  ( ZRHom ` R ) = U. ( ZZring RingHom R )
17 1 16 eqtri 
 |-  L = U. ( ZZring RingHom R )