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 20143
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 16590. Prime elements are closely related to irreducible elements (see df-irred 20073). (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 20142 . 2 class RPrime
2 vw . . 3 setvar 𝑀
3 cvv 3446 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class 𝑀
6 cbs 17084 . . . . 5 class Base
75, 6cfv 6497 . . . 4 class (Baseβ€˜π‘€)
8 vp . . . . . . . . . . 11 setvar 𝑝
98cv 1541 . . . . . . . . . 10 class 𝑝
10 vx . . . . . . . . . . . 12 setvar π‘₯
1110cv 1541 . . . . . . . . . . 11 class π‘₯
12 vy . . . . . . . . . . . 12 setvar 𝑦
1312cv 1541 . . . . . . . . . . 11 class 𝑦
14 cmulr 17135 . . . . . . . . . . . 12 class .r
155, 14cfv 6497 . . . . . . . . . . 11 class (.rβ€˜π‘€)
1611, 13, 15co 7358 . . . . . . . . . 10 class (π‘₯(.rβ€˜π‘€)𝑦)
17 vd . . . . . . . . . . 11 setvar 𝑑
1817cv 1541 . . . . . . . . . 10 class 𝑑
199, 16, 18wbr 5106 . . . . . . . . 9 wff 𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦)
209, 11, 18wbr 5106 . . . . . . . . . 10 wff 𝑝𝑑π‘₯
219, 13, 18wbr 5106 . . . . . . . . . 10 wff 𝑝𝑑𝑦
2220, 21wo 846 . . . . . . . . 9 wff (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦)
2319, 22wi 4 . . . . . . . 8 wff (𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))
24 cdsr 20068 . . . . . . . . 9 class βˆ₯r
255, 24cfv 6497 . . . . . . . 8 class (βˆ₯rβ€˜π‘€)
2623, 17, 25wsbc 3740 . . . . . . 7 wff [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))
274cv 1541 . . . . . . 7 class 𝑏
2826, 12, 27wral 3065 . . . . . 6 wff βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))
2928, 10, 27wral 3065 . . . . 5 wff βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))
30 cui 20069 . . . . . . . 8 class Unit
315, 30cfv 6497 . . . . . . 7 class (Unitβ€˜π‘€)
32 c0g 17322 . . . . . . . . 9 class 0g
335, 32cfv 6497 . . . . . . . 8 class (0gβ€˜π‘€)
3433csn 4587 . . . . . . 7 class {(0gβ€˜π‘€)}
3531, 34cun 3909 . . . . . 6 class ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)})
3627, 35cdif 3908 . . . . 5 class (𝑏 βˆ– ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)}))
3729, 8, 36crab 3408 . . . 4 class {𝑝 ∈ (𝑏 βˆ– ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)})) ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))}
384, 7, 37csb 3856 . . 3 class ⦋(Baseβ€˜π‘€) / π‘β¦Œ{𝑝 ∈ (𝑏 βˆ– ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)})) ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))}
392, 3, 38cmpt 5189 . 2 class (𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘€) / π‘β¦Œ{𝑝 ∈ (𝑏 βˆ– ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)})) ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))})
401, 39wceq 1542 1 wff RPrime = (𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘€) / π‘β¦Œ{𝑝 ∈ (𝑏 βˆ– ((Unitβ€˜π‘€) βˆͺ {(0gβ€˜π‘€)})) ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 [(βˆ₯rβ€˜π‘€) / 𝑑](𝑝𝑑(π‘₯(.rβ€˜π‘€)𝑦) β†’ (𝑝𝑑π‘₯ ∨ 𝑝𝑑𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  rprmval  32264
  Copyright terms: Public domain W3C validator