MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rprm Structured version   Visualization version   GIF version

Definition df-rprm 19392
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 16045. Prime elements are closely related to irreducible elements (see df-irred 19322). (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
StepHypRef Expression
1 crpm 19391 . 2 class RPrime
2 vw . . 3 setvar 𝑤
3 cvv 3492 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1527 . . . . 5 class 𝑤
6 cbs 16471 . . . . 5 class Base
75, 6cfv 6348 . . . 4 class (Base‘𝑤)
8 vp . . . . . . . . . . 11 setvar 𝑝
98cv 1527 . . . . . . . . . 10 class 𝑝
10 vx . . . . . . . . . . . 12 setvar 𝑥
1110cv 1527 . . . . . . . . . . 11 class 𝑥
12 vy . . . . . . . . . . . 12 setvar 𝑦
1312cv 1527 . . . . . . . . . . 11 class 𝑦
14 cmulr 16554 . . . . . . . . . . . 12 class .r
155, 14cfv 6348 . . . . . . . . . . 11 class (.r𝑤)
1611, 13, 15co 7145 . . . . . . . . . 10 class (𝑥(.r𝑤)𝑦)
17 vd . . . . . . . . . . 11 setvar 𝑑
1817cv 1527 . . . . . . . . . 10 class 𝑑
199, 16, 18wbr 5057 . . . . . . . . 9 wff 𝑝𝑑(𝑥(.r𝑤)𝑦)
209, 11, 18wbr 5057 . . . . . . . . . 10 wff 𝑝𝑑𝑥
219, 13, 18wbr 5057 . . . . . . . . . 10 wff 𝑝𝑑𝑦
2220, 21wo 841 . . . . . . . . 9 wff (𝑝𝑑𝑥𝑝𝑑𝑦)
2319, 22wi 4 . . . . . . . 8 wff (𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
24 cdsr 19317 . . . . . . . . 9 class r
255, 24cfv 6348 . . . . . . . 8 class (∥r𝑤)
2623, 17, 25wsbc 3769 . . . . . . 7 wff [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
274cv 1527 . . . . . . 7 class 𝑏
2826, 12, 27wral 3135 . . . . . 6 wff 𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
2928, 10, 27wral 3135 . . . . 5 wff 𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
30 cui 19318 . . . . . . . 8 class Unit
315, 30cfv 6348 . . . . . . 7 class (Unit‘𝑤)
32 c0g 16701 . . . . . . . . 9 class 0g
335, 32cfv 6348 . . . . . . . 8 class (0g𝑤)
3433csn 4557 . . . . . . 7 class {(0g𝑤)}
3531, 34cun 3931 . . . . . 6 class ((Unit‘𝑤) ∪ {(0g𝑤)})
3627, 35cdif 3930 . . . . 5 class (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)}))
3729, 8, 36crab 3139 . . . 4 class {𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))}
384, 7, 37csb 3880 . . 3 class (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))}
392, 3, 38cmpt 5137 . 2 class (𝑤 ∈ V ↦ (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))})
401, 39wceq 1528 1 wff RPrime = (𝑤 ∈ V ↦ (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator