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 = ℤRHom R
Assertion zrhval L = ring RingHom R

Proof

Step Hyp Ref Expression
1 zrhval.l L = ℤRHom R
2 oveq2 r = R ring RingHom r = ring RingHom R
3 2 unieqd r = R ring RingHom r = ring RingHom R
4 df-zrh ℤRHom = r V ring RingHom r
5 ovex ring RingHom R V
6 5 uniex ring RingHom R V
7 3 4 6 fvmpt R V ℤRHom R = ring RingHom R
8 fvprc ¬ R V ℤRHom R =
9 dfrhm2 RingHom = r Ring , s Ring r GrpHom s mulGrp r MndHom mulGrp s
10 9 reldmmpo Rel dom RingHom
11 10 ovprc2 ¬ R V ring RingHom R =
12 11 unieqd ¬ R V ring RingHom R =
13 uni0 =
14 12 13 eqtrdi ¬ R V ring RingHom R =
15 8 14 eqtr4d ¬ R V ℤRHom R = ring RingHom R
16 7 15 pm2.61i ℤRHom R = ring RingHom R
17 1 16 eqtri L = ring RingHom R