Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-zrng Unicode version

Definition df-zrng 23983
Description: Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-zrng  |- ZRing  =  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r ) ) )

Detailed syntax breakdown of Definition df-zrng
StepHypRef Expression
1 czr 23974 . 2  class ZRing
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . 4  class  r
5 czrh 16451 . . . . . 6  class  ZRHom
64, 5cfv 5255 . . . . 5  class  ( ZRHom `  r )
76crn 4690 . . . 4  class  ran  ( ZRHom `  r )
8 citr 23958 . . . 4  class IntgRing
94, 7, 8co 5858 . . 3  class  ( r IntgRing  ran  ( ZRHom `  r
) )
102, 3, 9cmpt 4077 . 2  class  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r
) ) )
111, 10wceq 1623 1  wff ZRing  =  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator