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

Definition df-prrngo 33017
 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 = {𝑟 ∈ RingOps ∣ {(GId‘(1st𝑟))} ∈ (PrIdl‘𝑟)}

Detailed syntax breakdown of Definition df-prrngo
StepHypRef Expression
1 cprrng 33015 . 2 class PrRing
2 vr . . . . . . . 8 setvar 𝑟
32cv 1474 . . . . . . 7 class 𝑟
4 c1st 7057 . . . . . . 7 class 1st
53, 4cfv 5804 . . . . . 6 class (1st𝑟)
6 cgi 26728 . . . . . 6 class GId
75, 6cfv 5804 . . . . 5 class (GId‘(1st𝑟))
87csn 4125 . . . 4 class {(GId‘(1st𝑟))}
9 cpridl 32977 . . . . 5 class PrIdl
103, 9cfv 5804 . . . 4 class (PrIdl‘𝑟)
118, 10wcel 1977 . . 3 wff {(GId‘(1st𝑟))} ∈ (PrIdl‘𝑟)
12 crngo 32863 . . 3 class RingOps
1311, 2, 12crab 2900 . 2 class {𝑟 ∈ RingOps ∣ {(GId‘(1st𝑟))} ∈ (PrIdl‘𝑟)}
141, 13wceq 1475 1 wff PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st𝑟))} ∈ (PrIdl‘𝑟)}
 Colors of variables: wff setvar class This definition is referenced by:  isprrngo  33019
 Copyright terms: Public domain W3C validator