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

Definition df-pridl 33477
 Description: Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see ispridl2 33504 and ispridlc 33536. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-pridl PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
Distinct variable group:   𝑖,𝑟,𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-pridl
StepHypRef Expression
1 cpridl 33474 . 2 class PrIdl
2 vr . . 3 setvar 𝑟
3 crngo 33360 . . 3 class RingOps
4 vi . . . . . . 7 setvar 𝑖
54cv 1479 . . . . . 6 class 𝑖
62cv 1479 . . . . . . . 8 class 𝑟
7 c1st 7118 . . . . . . . 8 class 1st
86, 7cfv 5852 . . . . . . 7 class (1st𝑟)
98crn 5080 . . . . . 6 class ran (1st𝑟)
105, 9wne 2790 . . . . 5 wff 𝑖 ≠ ran (1st𝑟)
11 vx . . . . . . . . . . . . 13 setvar 𝑥
1211cv 1479 . . . . . . . . . . . 12 class 𝑥
13 vy . . . . . . . . . . . . 13 setvar 𝑦
1413cv 1479 . . . . . . . . . . . 12 class 𝑦
15 c2nd 7119 . . . . . . . . . . . . 13 class 2nd
166, 15cfv 5852 . . . . . . . . . . . 12 class (2nd𝑟)
1712, 14, 16co 6610 . . . . . . . . . . 11 class (𝑥(2nd𝑟)𝑦)
1817, 5wcel 1987 . . . . . . . . . 10 wff (𝑥(2nd𝑟)𝑦) ∈ 𝑖
19 vb . . . . . . . . . . 11 setvar 𝑏
2019cv 1479 . . . . . . . . . 10 class 𝑏
2118, 13, 20wral 2907 . . . . . . . . 9 wff 𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖
22 va . . . . . . . . . 10 setvar 𝑎
2322cv 1479 . . . . . . . . 9 class 𝑎
2421, 11, 23wral 2907 . . . . . . . 8 wff 𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖
2523, 5wss 3559 . . . . . . . . 9 wff 𝑎𝑖
2620, 5wss 3559 . . . . . . . . 9 wff 𝑏𝑖
2725, 26wo 383 . . . . . . . 8 wff (𝑎𝑖𝑏𝑖)
2824, 27wi 4 . . . . . . 7 wff (∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
29 cidl 33473 . . . . . . . 8 class Idl
306, 29cfv 5852 . . . . . . 7 class (Idl‘𝑟)
3128, 19, 30wral 2907 . . . . . 6 wff 𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
3231, 22, 30wral 2907 . . . . 5 wff 𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
3310, 32wa 384 . . . 4 wff (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))
3433, 4, 30crab 2911 . . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))}
352, 3, 34cmpt 4678 . 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
361, 35wceq 1480 1 wff PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(2nd𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
 Colors of variables: wff setvar class This definition is referenced by:  pridlval  33499
 Copyright terms: Public domain W3C validator