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		cirng	|- 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 ) ) )