Metamath Proof Explorer


Definition df-zrng

Description: Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-zrng
|- ZRing = ( r e. _V |-> ( r IntgRing ran ( ZRHom ` r ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czr
 |-  ZRing
1 vr
 |-  r
2 cvv
 |-  _V
3 1 cv
 |-  r
4 citr
 |-  IntgRing
5 czrh
 |-  ZRHom
6 3 5 cfv
 |-  ( ZRHom ` r )
7 6 crn
 |-  ran ( ZRHom ` r )
8 3 7 4 co
 |-  ( r IntgRing ran ( ZRHom ` r ) )
9 1 2 8 cmpt
 |-  ( r e. _V |-> ( r IntgRing ran ( ZRHom ` r ) ) )
10 0 9 wceq
 |-  ZRing = ( r e. _V |-> ( r IntgRing ran ( ZRHom ` r ) ) )