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

Definition df-irred 20258
Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
Assertion
Ref Expression
df-irred Irred = (𝑀 ∈ V ↦ ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧})
Distinct variable group:   𝑀,𝑏,π‘₯,𝑦,𝑧

Detailed syntax breakdown of Definition df-irred
StepHypRef Expression
1 cir 20255 . 2 class Irred
2 vw . . 3 setvar 𝑀
3 cvv 3468 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1532 . . . . . 6 class 𝑀
6 cbs 17150 . . . . . 6 class Base
75, 6cfv 6536 . . . . 5 class (Baseβ€˜π‘€)
8 cui 20254 . . . . . 6 class Unit
95, 8cfv 6536 . . . . 5 class (Unitβ€˜π‘€)
107, 9cdif 3940 . . . 4 class ((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€))
11 vx . . . . . . . . . 10 setvar π‘₯
1211cv 1532 . . . . . . . . 9 class π‘₯
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1532 . . . . . . . . 9 class 𝑦
15 cmulr 17204 . . . . . . . . . 10 class .r
165, 15cfv 6536 . . . . . . . . 9 class (.rβ€˜π‘€)
1712, 14, 16co 7404 . . . . . . . 8 class (π‘₯(.rβ€˜π‘€)𝑦)
18 vz . . . . . . . . 9 setvar 𝑧
1918cv 1532 . . . . . . . 8 class 𝑧
2017, 19wne 2934 . . . . . . 7 wff (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧
214cv 1532 . . . . . . 7 class 𝑏
2220, 13, 21wral 3055 . . . . . 6 wff βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧
2322, 11, 21wral 3055 . . . . 5 wff βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧
2423, 18, 21crab 3426 . . . 4 class {𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧}
254, 10, 24csb 3888 . . 3 class ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧}
262, 3, 25cmpt 5224 . 2 class (𝑀 ∈ V ↦ ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧})
271, 26wceq 1533 1 wff Irred = (𝑀 ∈ V ↦ ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧})
Colors of variables: wff setvar class
This definition is referenced by:  isirred  20318
  Copyright terms: Public domain W3C validator