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 32256
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 32261 and isprmidlc 32268. (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 32255 . 2 class PrmIdeal
2 vr . . 3 setvar π‘Ÿ
3 crg 19969 . . 3 class Ring
4 vi . . . . . . 7 setvar 𝑖
54cv 1541 . . . . . 6 class 𝑖
62cv 1541 . . . . . . 7 class π‘Ÿ
7 cbs 17088 . . . . . . 7 class Base
86, 7cfv 6497 . . . . . 6 class (Baseβ€˜π‘Ÿ)
95, 8wne 2940 . . . . 5 wff 𝑖 β‰  (Baseβ€˜π‘Ÿ)
10 vx . . . . . . . . . . . . 13 setvar π‘₯
1110cv 1541 . . . . . . . . . . . 12 class π‘₯
12 vy . . . . . . . . . . . . 13 setvar 𝑦
1312cv 1541 . . . . . . . . . . . 12 class 𝑦
14 cmulr 17139 . . . . . . . . . . . . 13 class .r
156, 14cfv 6497 . . . . . . . . . . . 12 class (.rβ€˜π‘Ÿ)
1611, 13, 15co 7358 . . . . . . . . . . 11 class (π‘₯(.rβ€˜π‘Ÿ)𝑦)
1716, 5wcel 2107 . . . . . . . . . 10 wff (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖
18 vb . . . . . . . . . . 11 setvar 𝑏
1918cv 1541 . . . . . . . . . 10 class 𝑏
2017, 12, 19wral 3061 . . . . . . . . 9 wff βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖
21 va . . . . . . . . . 10 setvar π‘Ž
2221cv 1541 . . . . . . . . 9 class π‘Ž
2320, 10, 22wral 3061 . . . . . . . 8 wff βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖
2422, 5wss 3911 . . . . . . . . 9 wff π‘Ž βŠ† 𝑖
2519, 5wss 3911 . . . . . . . . 9 wff 𝑏 βŠ† 𝑖
2624, 25wo 846 . . . . . . . 8 wff (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖)
2723, 26wi 4 . . . . . . 7 wff (βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖))
28 clidl 20647 . . . . . . . 8 class LIdeal
296, 28cfv 6497 . . . . . . 7 class (LIdealβ€˜π‘Ÿ)
3027, 18, 29wral 3061 . . . . . 6 wff βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖))
3130, 21, 29wral 3061 . . . . 5 wff βˆ€π‘Ž ∈ (LIdealβ€˜π‘Ÿ)βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖))
329, 31wa 397 . . . 4 wff (𝑖 β‰  (Baseβ€˜π‘Ÿ) ∧ βˆ€π‘Ž ∈ (LIdealβ€˜π‘Ÿ)βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖)))
3332, 4, 29crab 3406 . . 3 class {𝑖 ∈ (LIdealβ€˜π‘Ÿ) ∣ (𝑖 β‰  (Baseβ€˜π‘Ÿ) ∧ βˆ€π‘Ž ∈ (LIdealβ€˜π‘Ÿ)βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖)))}
342, 3, 33cmpt 5189 . 2 class (π‘Ÿ ∈ Ring ↦ {𝑖 ∈ (LIdealβ€˜π‘Ÿ) ∣ (𝑖 β‰  (Baseβ€˜π‘Ÿ) ∧ βˆ€π‘Ž ∈ (LIdealβ€˜π‘Ÿ)βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖)))})
351, 34wceq 1542 1 wff PrmIdeal = (π‘Ÿ ∈ Ring ↦ {𝑖 ∈ (LIdealβ€˜π‘Ÿ) ∣ (𝑖 β‰  (Baseβ€˜π‘Ÿ) ∧ βˆ€π‘Ž ∈ (LIdealβ€˜π‘Ÿ)βˆ€π‘ ∈ (LIdealβ€˜π‘Ÿ)(βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘Ÿ)𝑦) ∈ 𝑖 β†’ (π‘Ž βŠ† 𝑖 ∨ 𝑏 βŠ† 𝑖)))})
Colors of variables: wff setvar class
This definition is referenced by:  prmidlval  32257
  Copyright terms: Public domain W3C validator