Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prrngo Structured version   Unicode version

Definition df-prrngo 26660
Description: Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-prrngo  |-  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }

Detailed syntax breakdown of Definition df-prrngo
StepHypRef Expression
1 cprrng 26658 . 2  class  PrRing
2 vr . . . . . . . 8  set  r
32cv 1652 . . . . . . 7  class  r
4 c1st 6349 . . . . . . 7  class  1st
53, 4cfv 5456 . . . . . 6  class  ( 1st `  r )
6 cgi 21777 . . . . . 6  class GId
75, 6cfv 5456 . . . . 5  class  (GId `  ( 1st `  r ) )
87csn 3816 . . . 4  class  { (GId
`  ( 1st `  r
) ) }
9 cpridl 26620 . . . . 5  class  PrIdl
103, 9cfv 5456 . . . 4  class  ( PrIdl `  r )
118, 10wcel 1726 . . 3  wff  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r )
12 crngo 21965 . . 3  class  RingOps
1311, 2, 12crab 2711 . 2  class  { r  e.  RingOps  |  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r ) }
141, 13wceq 1653 1  wff  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }
Colors of variables: wff set class
This definition is referenced by:  isprrngo  26662
  Copyright terms: Public domain W3C validator