df-prrngo - Mathbox for Jeff Madsen

	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 35318

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‘(1^st ‘𝑟))} ∈ (PrIdl‘𝑟)}

**Detailed syntax breakdown of Definition df-prrngo**
Step	Hyp	Ref	Expression
1		cprrng 35316	. 2 class PrRing
2		vr	. . . . . . . 8 setvar 𝑟
3	2	cv 1530	. . . . . . 7 class 𝑟
4		c1st 7679	. . . . . . 7 class 1^st
5	3, 4	cfv 6348	. . . . . 6 class (1^st ‘𝑟)
6		cgi 28259	. . . . . 6 class GId
7	5, 6	cfv 6348	. . . . 5 class (GId‘(1^st ‘𝑟))
8	7	csn 4559	. . . 4 class {(GId‘(1^st ‘𝑟))}
9		cpridl 35278	. . . . 5 class PrIdl
10	3, 9	cfv 6348	. . . 4 class (PrIdl‘𝑟)
11	8, 10	wcel 2108	. . 3 wff {(GId‘(1^st ‘𝑟))} ∈ (PrIdl‘𝑟)
12		crngo 35164	. . 3 class RingOps
13	11, 2, 12	crab 3140	. 2 class {𝑟 ∈ RingOps ∣ {(GId‘(1^st ‘𝑟))} ∈ (PrIdl‘𝑟)}
14	1, 13	wceq 1531	1 wff PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1^st ‘𝑟))} ∈ (PrIdl‘𝑟)}

Colors of variables: wff setvar class

This definition is referenced by: isprrngo 35320