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

Definition df-zrng 24267
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 24258 . 2  class ZRing
2 vr . . 3  set  r
3 cvv 2822 . . 3  class  _V
42cv 1632 . . . 4  class  r
5 czrh 16507 . . . . . 6  class  ZRHom
64, 5cfv 5292 . . . . 5  class  ( ZRHom `  r )
76crn 4727 . . . 4  class  ran  ( ZRHom `  r )
8 citr 24242 . . . 4  class IntgRing
94, 7, 8co 5900 . . 3  class  ( r IntgRing  ran  ( ZRHom `  r
) )
102, 3, 9cmpt 4114 . 2  class  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r
) ) )
111, 10wceq 1633 1  wff ZRing  =  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator