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 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion zrhval 𝐿 = ∪ ( ℤring RingHom 𝑅 )

Proof

Step Hyp Ref Expression
1 zrhval.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2 oveq2 ⊢ ( 𝑟 = 𝑅 → ( ℤring RingHom 𝑟 ) = ( ℤring RingHom 𝑅 ) )
3 2 unieqd ⊢ ( 𝑟 = 𝑅 → ∪ ( ℤring RingHom 𝑟 ) = ∪ ( ℤring RingHom 𝑅 ) )
4 df-zrh ⊢ ℤRHom = ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )
5 ovex ⊢ ( ℤring RingHom 𝑅 ) ∈ V
6 5 uniex ⊢ ∪ ( ℤring RingHom 𝑅 ) ∈ V
7 3 4 6 fvmpt ⊢ ( 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 ) )
8 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∅ )
9 dfrhm2 ⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
10 9 reldmmpo ⊢ Rel dom RingHom
11 10 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( ℤring RingHom 𝑅 ) = ∅ )
12 11 unieqd ⊢ ( ¬ 𝑅 ∈ V → ∪ ( ℤring RingHom 𝑅 ) = ∪ ∅ )
13 uni0 ⊢ ∪ ∅ = ∅
14 12 13 eqtrdi ⊢ ( ¬ 𝑅 ∈ V → ∪ ( ℤring RingHom 𝑅 ) = ∅ )
15 8 14 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 ) )
16 7 15 pm2.61i ⊢ ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 )
17 1 16 eqtri ⊢ 𝐿 = ∪ ( ℤring RingHom 𝑅 )