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 30275
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 30273 . 2  class  PrRing
2 vr . . . . . . . 8  setvar  r
32cv 1378 . . . . . . 7  class  r
4 c1st 6783 . . . . . . 7  class  1st
53, 4cfv 5588 . . . . . 6  class  ( 1st `  r )
6 cgi 24962 . . . . . 6  class GId
75, 6cfv 5588 . . . . 5  class  (GId `  ( 1st `  r ) )
87csn 4027 . . . 4  class  { (GId
`  ( 1st `  r
) ) }
9 cpridl 30235 . . . . 5  class  PrIdl
103, 9cfv 5588 . . . 4  class  ( PrIdl `  r )
118, 10wcel 1767 . . 3  wff  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r )
12 crngo 25150 . . 3  class  RingOps
1311, 2, 12crab 2818 . 2  class  { r  e.  RingOps  |  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r ) }
141, 13wceq 1379 1  wff  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }
Colors of variables: wff setvar class
This definition is referenced by:  isprrngo  30277
  Copyright terms: Public domain W3C validator