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 
|- ZRHom = ( r e. _V |-> U. ( ZZring RingHom r ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czrh 
 |-  ZRHom
1 vr 
 |-  r
2 cvv 
 |-  _V
3 zring 
 |-  ZZring
4 crh 
 |-  RingHom
5 1 cv 
 |-  r
6 3 5 4 co 
 |-  ( ZZring RingHom r )
7 6 cuni 
 |-  U. ( ZZring RingHom r )
8 1 2 7 cmpt 
 |-  ( r e. _V |-> U. ( ZZring RingHom r ) )
9 0 8 wceq 
 |-  ZRHom = ( r e. _V |-> U. ( ZZring RingHom r ) )