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

Definition df-rprm 19462
 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 16049. Prime elements are closely related to irreducible elements (see df-irred 19392). (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 19461 . 2 class RPrime
2 vw . . 3 setvar 𝑤
3 cvv 3441 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1537 . . . . 5 class 𝑤
6 cbs 16477 . . . . 5 class Base
75, 6cfv 6324 . . . 4 class (Base‘𝑤)
8 vp . . . . . . . . . . 11 setvar 𝑝
98cv 1537 . . . . . . . . . 10 class 𝑝
10 vx . . . . . . . . . . . 12 setvar 𝑥
1110cv 1537 . . . . . . . . . . 11 class 𝑥
12 vy . . . . . . . . . . . 12 setvar 𝑦
1312cv 1537 . . . . . . . . . . 11 class 𝑦
14 cmulr 16560 . . . . . . . . . . . 12 class .r
155, 14cfv 6324 . . . . . . . . . . 11 class (.r𝑤)
1611, 13, 15co 7135 . . . . . . . . . 10 class (𝑥(.r𝑤)𝑦)
17 vd . . . . . . . . . . 11 setvar 𝑑
1817cv 1537 . . . . . . . . . 10 class 𝑑
199, 16, 18wbr 5030 . . . . . . . . 9 wff 𝑝𝑑(𝑥(.r𝑤)𝑦)
209, 11, 18wbr 5030 . . . . . . . . . 10 wff 𝑝𝑑𝑥
219, 13, 18wbr 5030 . . . . . . . . . 10 wff 𝑝𝑑𝑦
2220, 21wo 844 . . . . . . . . 9 wff (𝑝𝑑𝑥𝑝𝑑𝑦)
2319, 22wi 4 . . . . . . . 8 wff (𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
24 cdsr 19387 . . . . . . . . 9 class r
255, 24cfv 6324 . . . . . . . 8 class (∥r𝑤)
2623, 17, 25wsbc 3720 . . . . . . 7 wff [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
274cv 1537 . . . . . . 7 class 𝑏
2826, 12, 27wral 3106 . . . . . 6 wff 𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
2928, 10, 27wral 3106 . . . . 5 wff 𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))
30 cui 19388 . . . . . . . 8 class Unit
315, 30cfv 6324 . . . . . . 7 class (Unit‘𝑤)
32 c0g 16707 . . . . . . . . 9 class 0g
335, 32cfv 6324 . . . . . . . 8 class (0g𝑤)
3433csn 4525 . . . . . . 7 class {(0g𝑤)}
3531, 34cun 3879 . . . . . 6 class ((Unit‘𝑤) ∪ {(0g𝑤)})
3627, 35cdif 3878 . . . . 5 class (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)}))
3729, 8, 36crab 3110 . . . 4 class {𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))}
384, 7, 37csb 3828 . . 3 class (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))}
392, 3, 38cmpt 5110 . 2 class (𝑤 ∈ V ↦ (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))})
401, 39wceq 1538 1 wff RPrime = (𝑤 ∈ V ↦ (Base‘𝑤) / 𝑏{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g𝑤)})) ∣ ∀𝑥𝑏𝑦𝑏 [(∥r𝑤) / 𝑑](𝑝𝑑(𝑥(.r𝑤)𝑦) → (𝑝𝑑𝑥𝑝𝑑𝑦))})
 Colors of variables: wff setvar class This definition is referenced by:  rprmval  31079
 Copyright terms: Public domain W3C validator