Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prmidl Structured version   Visualization version   GIF version

Definition df-prmidl 30992
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 prmidl2 30997 and isprmidlc 31004. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.)
Assertion
Ref Expression
df-prmidl PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
Distinct variable group:   𝑖,𝑟,𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-prmidl
StepHypRef Expression
1 cprmidl 30991 . 2 class PrmIdeal
2 vr . . 3 setvar 𝑟
3 crg 19297 . . 3 class Ring
4 vi . . . . . . 7 setvar 𝑖
54cv 1537 . . . . . 6 class 𝑖
62cv 1537 . . . . . . 7 class 𝑟
7 cbs 16483 . . . . . . 7 class Base
86, 7cfv 6343 . . . . . 6 class (Base‘𝑟)
95, 8wne 3014 . . . . 5 wff 𝑖 ≠ (Base‘𝑟)
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1537 . . . . . . . . . . . 12 class 𝑥
12 vy . . . . . . . . . . . . 13 setvar 𝑦
1312cv 1537 . . . . . . . . . . . 12 class 𝑦
14 cmulr 16566 . . . . . . . . . . . . 13 class .r
156, 14cfv 6343 . . . . . . . . . . . 12 class (.r𝑟)
1611, 13, 15co 7149 . . . . . . . . . . 11 class (𝑥(.r𝑟)𝑦)
1716, 5wcel 2115 . . . . . . . . . 10 wff (𝑥(.r𝑟)𝑦) ∈ 𝑖
18 vb . . . . . . . . . . 11 setvar 𝑏
1918cv 1537 . . . . . . . . . 10 class 𝑏
2017, 12, 19wral 3133 . . . . . . . . 9 wff 𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖
21 va . . . . . . . . . 10 setvar 𝑎
2221cv 1537 . . . . . . . . 9 class 𝑎
2320, 10, 22wral 3133 . . . . . . . 8 wff 𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖
2422, 5wss 3919 . . . . . . . . 9 wff 𝑎𝑖
2519, 5wss 3919 . . . . . . . . 9 wff 𝑏𝑖
2624, 25wo 844 . . . . . . . 8 wff (𝑎𝑖𝑏𝑖)
2723, 26wi 4 . . . . . . 7 wff (∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
28 clidl 19942 . . . . . . . 8 class LIdeal
296, 28cfv 6343 . . . . . . 7 class (LIdeal‘𝑟)
3027, 18, 29wral 3133 . . . . . 6 wff 𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
3130, 21, 29wral 3133 . . . . 5 wff 𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖))
329, 31wa 399 . . . 4 wff (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))
3332, 4, 29crab 3137 . . 3 class {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))}
342, 3, 33cmpt 5132 . 2 class (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
351, 34wceq 1538 1 wff PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥𝑎𝑦𝑏 (𝑥(.r𝑟)𝑦) ∈ 𝑖 → (𝑎𝑖𝑏𝑖)))})
Colors of variables: wff setvar class
This definition is referenced by:  prmidlval  30993
  Copyright terms: Public domain W3C validator