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

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