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

Metamath Proof Explorer

Definition df-zrh

Description: Define the unique homomorphism from the integers into a ring. This encodes the usual notation of n = 1r + 1r + ... + 1r for integers (see also df-mulg ). (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Assertion df-zrh ℤRHom = ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czrh ⊢ ℤRHom
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 czring ⊢ ℤring
4 crh ⊢ RingHom
5 1 cv ⊢ 𝑟
6 3 5 4 co ⊢ ( ℤring RingHom 𝑟 )
7 6 cuni ⊢ ∪ ( ℤring RingHom 𝑟 )
8 1 2 7 cmpt ⊢ ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )
9 0 8 wceq ⊢ ℤRHom = ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )