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

Definition df-zrng 25089
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 25080 . 2  class ZRing
2 vr . . 3  set  r
3 cvv 2958 . . 3  class  _V
42cv 1652 . . . 4  class  r
5 czrh 16780 . . . . . 6  class  ZRHom
64, 5cfv 5456 . . . . 5  class  ( ZRHom `  r )
76crn 4881 . . . 4  class  ran  ( ZRHom `  r )
8 citr 25064 . . . 4  class IntgRing
94, 7, 8co 6083 . . 3  class  ( r IntgRing  ran  ( ZRHom `  r
) )
102, 3, 9cmpt 4268 . 2  class  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r
) ) )
111, 10wceq 1653 1  wff ZRing  =  ( r  e.  _V  |->  ( r IntgRing  ran  ( ZRHom `  r ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator