Users' Mathboxes 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 36911
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 36909 . 2 class PrRing
2 vr . . . . . . . 8 setvar π‘Ÿ
32cv 1540 . . . . . . 7 class π‘Ÿ
4 c1st 7972 . . . . . . 7 class 1st
53, 4cfv 6543 . . . . . 6 class (1st β€˜π‘Ÿ)
6 cgi 29738 . . . . . 6 class GId
75, 6cfv 6543 . . . . 5 class (GIdβ€˜(1st β€˜π‘Ÿ))
87csn 4628 . . . 4 class {(GIdβ€˜(1st β€˜π‘Ÿ))}
9 cpridl 36871 . . . . 5 class PrIdl
103, 9cfv 6543 . . . 4 class (PrIdlβ€˜π‘Ÿ)
118, 10wcel 2106 . . 3 wff {(GIdβ€˜(1st β€˜π‘Ÿ))} ∈ (PrIdlβ€˜π‘Ÿ)
12 crngo 36757 . . 3 class RingOps
1311, 2, 12crab 3432 . 2 class {π‘Ÿ ∈ RingOps ∣ {(GIdβ€˜(1st β€˜π‘Ÿ))} ∈ (PrIdlβ€˜π‘Ÿ)}
141, 13wceq 1541 1 wff PrRing = {π‘Ÿ ∈ RingOps ∣ {(GIdβ€˜(1st β€˜π‘Ÿ))} ∈ (PrIdlβ€˜π‘Ÿ)}
Colors of variables: wff setvar class
This definition is referenced by:  isprrngo  36913
  Copyright terms: Public domain W3C validator