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	$$⊢\mathrm{\mathbb{Z}Ring}=\left(r\in \mathrm{V}⟼r\mathrm{IntgRing}\mathrm{ran}\mathrm{\mathbb{Z}RHom}\left(r\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czr	$$class\mathrm{\mathbb{Z}Ring}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarr$$
4		cirng	$$class\mathrm{IntgRing}$$
5		czrh	$$class\mathrm{\mathbb{Z}RHom}$$
6	3 5	cfv	$$class\mathrm{\mathbb{Z}RHom}\left(r\right)$$
7	6	crn	$$class\mathrm{ran}\mathrm{\mathbb{Z}RHom}\left(r\right)$$
8	3 7 4	co	$$class\left(r\mathrm{IntgRing}\mathrm{ran}\mathrm{\mathbb{Z}RHom}\left(r\right)\right)$$
9	1 2 8	cmpt	$$class\left(r\in \mathrm{V}⟼r\mathrm{IntgRing}\mathrm{ran}\mathrm{\mathbb{Z}RHom}\left(r\right)\right)$$
10	0 9	wceq	$$wff\mathrm{\mathbb{Z}Ring}=\left(r\in \mathrm{V}⟼r\mathrm{IntgRing}\mathrm{ran}\mathrm{\mathbb{Z}RHom}\left(r\right)\right)$$