Definition df-prmidl 31019

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 31024 and isprmidlc 31031. (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

Step	Hyp	Ref	Expression
1		cprmidl 31018	. 2 class PrmIdeal
2		vr	. . 3 setvar 𝑟
3		crg 19290	. . 3 class Ring
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1537	. . . . . 6 class 𝑖
6	2	cv 1537	. . . . . . 7 class 𝑟
7		cbs 16475	. . . . . . 7 class Base
8	6, 7	cfv 6324	. . . . . 6 class (Base‘𝑟)
9	5, 8	wne 2987	. . . . 5 wff 𝑖 ≠ (Base‘𝑟)
10		vx	. . . . . . . . . . . . 13 setvar 𝑥
11	10	cv 1537	. . . . . . . . . . . 12 class 𝑥
12		vy	. . . . . . . . . . . . 13 setvar 𝑦
13	12	cv 1537	. . . . . . . . . . . 12 class 𝑦
14		cmulr 16558	. . . . . . . . . . . . 13 class .r
15	6, 14	cfv 6324	. . . . . . . . . . . 12 class (.r‘𝑟)
16	11, 13, 15	co 7135	. . . . . . . . . . 11 class (𝑥(.r‘𝑟)𝑦)
17	16, 5	wcel 2111	. . . . . . . . . 10 wff (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
18		vb	. . . . . . . . . . 11 setvar 𝑏
19	18	cv 1537	. . . . . . . . . 10 class 𝑏
20	17, 12, 19	wral 3106	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
21		va	. . . . . . . . . 10 setvar 𝑎
22	21	cv 1537	. . . . . . . . 9 class 𝑎
23	20, 10, 22	wral 3106	. . . . . . . 8 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
24	22, 5	wss 3881	. . . . . . . . 9 wff 𝑎 ⊆ 𝑖
25	19, 5	wss 3881	. . . . . . . . 9 wff 𝑏 ⊆ 𝑖
26	24, 25	wo 844	. . . . . . . 8 wff (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)
27	23, 26	wi 4	. . . . . . 7 wff (∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
28		clidl 19935	. . . . . . . 8 class LIdeal
29	6, 28	cfv 6324	. . . . . . 7 class (LIdeal‘𝑟)
30	27, 18, 29	wral 3106	. . . . . 6 wff ∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
31	30, 21, 29	wral 3106	. . . . 5 wff ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
32	9, 31	wa 399	. . . 4 wff (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))
33	32, 4, 29	crab 3110	. . 3 class {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}
34	2, 3, 33	cmpt 5110	. 2 class (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
35	1, 34	wceq 1538	1 wff PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})

This definition is referenced by:  prmidlval  31020