Definition df-prmidl 31513

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 31518 and isprmidlc 31525. (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 31512	. 2 class PrmIdeal
2		vr	. . 3 setvar 𝑟
3		crg 19698	. . 3 class Ring
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1538	. . . . . 6 class 𝑖
6	2	cv 1538	. . . . . . 7 class 𝑟
7		cbs 16840	. . . . . . 7 class Base
8	6, 7	cfv 6418	. . . . . 6 class (Base‘𝑟)
9	5, 8	wne 2942	. . . . 5 wff 𝑖 ≠ (Base‘𝑟)
10		vx	. . . . . . . . . . . . 13 setvar 𝑥
11	10	cv 1538	. . . . . . . . . . . 12 class 𝑥
12		vy	. . . . . . . . . . . . 13 setvar 𝑦
13	12	cv 1538	. . . . . . . . . . . 12 class 𝑦
14		cmulr 16889	. . . . . . . . . . . . 13 class .r
15	6, 14	cfv 6418	. . . . . . . . . . . 12 class (.r‘𝑟)
16	11, 13, 15	co 7255	. . . . . . . . . . 11 class (𝑥(.r‘𝑟)𝑦)
17	16, 5	wcel 2108	. . . . . . . . . 10 wff (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
18		vb	. . . . . . . . . . 11 setvar 𝑏
19	18	cv 1538	. . . . . . . . . 10 class 𝑏
20	17, 12, 19	wral 3063	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
21		va	. . . . . . . . . 10 setvar 𝑎
22	21	cv 1538	. . . . . . . . 9 class 𝑎
23	20, 10, 22	wral 3063	. . . . . . . 8 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖
24	22, 5	wss 3883	. . . . . . . . 9 wff 𝑎 ⊆ 𝑖
25	19, 5	wss 3883	. . . . . . . . 9 wff 𝑏 ⊆ 𝑖
26	24, 25	wo 843	. . . . . . . 8 wff (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)
27	23, 26	wi 4	. . . . . . 7 wff (∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
28		clidl 20347	. . . . . . . 8 class LIdeal
29	6, 28	cfv 6418	. . . . . . 7 class (LIdeal‘𝑟)
30	27, 18, 29	wral 3063	. . . . . 6 wff ∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
31	30, 21, 29	wral 3063	. . . . 5 wff ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
32	9, 31	wa 395	. . . 4 wff (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))
33	32, 4, 29	crab 3067	. . 3 class {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}
34	2, 3, 33	cmpt 5153	. 2 class (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
35	1, 34	wceq 1539	1 wff PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})

This definition is referenced by:  prmidlval  31514