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 = ( 𝑟 ∈ V ↦ ( 𝑟 IntgRing ran ( ℤRHom ‘ 𝑟 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czr	⊢ ZRing
1		vr	⊢ 𝑟
2		cvv	⊢ V
3	1	cv	⊢ 𝑟
4		citr	⊢ IntgRing
5		czrh	⊢ ℤRHom
6	3 5	cfv	⊢ ( ℤRHom ‘ 𝑟 )
7	6	crn	⊢ ran ( ℤRHom ‘ 𝑟 )
8	3 7 4	co	⊢ ( 𝑟 IntgRing ran ( ℤRHom ‘ 𝑟 ) )
9	1 2 8	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑟 IntgRing ran ( ℤRHom ‘ 𝑟 ) ) )
10	0 9	wceq	⊢ ZRing = ( 𝑟 ∈ V ↦ ( 𝑟 IntgRing ran ( ℤRHom ‘ 𝑟 ) ) )