Definition df-rprm 19955

Description: Define the function associating with a ring its set of prime elements. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 16418. Prime elements are closely related to irreducible elements (see df-irred 19885). (Contributed by Mario Carneiro, 17-Feb-2015.)

Assertion

Ref	Expression
df-rprm	⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})

Distinct variable group:   𝑏,𝑑,𝑝,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-rprm

Step	Hyp	Ref	Expression
1		crpm 19954	. 2 class RPrime
2		vw	. . 3 setvar 𝑤
3		cvv 3432	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . 5 class 𝑤
6		cbs 16912	. . . . 5 class Base
7	5, 6	cfv 6433	. . . 4 class (Base‘𝑤)
8		vp	. . . . . . . . . . 11 setvar 𝑝
9	8	cv 1538	. . . . . . . . . 10 class 𝑝
10		vx	. . . . . . . . . . . 12 setvar 𝑥
11	10	cv 1538	. . . . . . . . . . 11 class 𝑥
12		vy	. . . . . . . . . . . 12 setvar 𝑦
13	12	cv 1538	. . . . . . . . . . 11 class 𝑦
14		cmulr 16963	. . . . . . . . . . . 12 class .r
15	5, 14	cfv 6433	. . . . . . . . . . 11 class (.r‘𝑤)
16	11, 13, 15	co 7275	. . . . . . . . . 10 class (𝑥(.r‘𝑤)𝑦)
17		vd	. . . . . . . . . . 11 setvar 𝑑
18	17	cv 1538	. . . . . . . . . 10 class 𝑑
19	9, 16, 18	wbr 5074	. . . . . . . . 9 wff 𝑝𝑑(𝑥(.r‘𝑤)𝑦)
20	9, 11, 18	wbr 5074	. . . . . . . . . 10 wff 𝑝𝑑𝑥
21	9, 13, 18	wbr 5074	. . . . . . . . . 10 wff 𝑝𝑑𝑦
22	20, 21	wo 844	. . . . . . . . 9 wff (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)
23	19, 22	wi 4	. . . . . . . 8 wff (𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))
24		cdsr 19880	. . . . . . . . 9 class ∥r
25	5, 24	cfv 6433	. . . . . . . 8 class (∥r‘𝑤)
26	23, 17, 25	wsbc 3716	. . . . . . 7 wff [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))
27	4	cv 1538	. . . . . . 7 class 𝑏
28	26, 12, 27	wral 3064	. . . . . 6 wff ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))
29	28, 10, 27	wral 3064	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))
30		cui 19881	. . . . . . . 8 class Unit
31	5, 30	cfv 6433	. . . . . . 7 class (Unit‘𝑤)
32		c0g 17150	. . . . . . . . 9 class 0g
33	5, 32	cfv 6433	. . . . . . . 8 class (0g‘𝑤)
34	33	csn 4561	. . . . . . 7 class {(0g‘𝑤)}
35	31, 34	cun 3885	. . . . . 6 class ((Unit‘𝑤) ∪ {(0g‘𝑤)})
36	27, 35	cdif 3884	. . . . 5 class (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)}))
37	29, 8, 36	crab 3068	. . . 4 class {𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}
38	4, 7, 37	csb 3832	. . 3 class ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}
39	2, 3, 38	cmpt 5157	. 2 class (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})
40	1, 39	wceq 1539	1 wff RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})

This definition is referenced by:  rprmval  31664