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 18689
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 18686 . 2 class Irred
2 vw . . 3 setvar 𝑤
3 cvv 3231 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1522 . . . . . 6 class 𝑤
6 cbs 15904 . . . . . 6 class Base
75, 6cfv 5926 . . . . 5 class (Base‘𝑤)
8 cui 18685 . . . . . 6 class Unit
95, 8cfv 5926 . . . . 5 class (Unit‘𝑤)
107, 9cdif 3604 . . . 4 class ((Base‘𝑤) ∖ (Unit‘𝑤))
11 vx . . . . . . . . . 10 setvar 𝑥
1211cv 1522 . . . . . . . . 9 class 𝑥
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1522 . . . . . . . . 9 class 𝑦
15 cmulr 15989 . . . . . . . . . 10 class .r
165, 15cfv 5926 . . . . . . . . 9 class (.r𝑤)
1712, 14, 16co 6690 . . . . . . . 8 class (𝑥(.r𝑤)𝑦)
18 vz . . . . . . . . 9 setvar 𝑧
1918cv 1522 . . . . . . . 8 class 𝑧
2017, 19wne 2823 . . . . . . 7 wff (𝑥(.r𝑤)𝑦) ≠ 𝑧
214cv 1522 . . . . . . 7 class 𝑏
2220, 13, 21wral 2941 . . . . . 6 wff 𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧
2322, 11, 21wral 2941 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧
2423, 18, 21crab 2945 . . . 4 class {𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧}
254, 10, 24csb 3566 . . 3 class ((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧}
262, 3, 25cmpt 4762 . 2 class (𝑤 ∈ V ↦ ((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧})
271, 26wceq 1523 1 wff Irred = (𝑤 ∈ V ↦ ((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧})
Colors of variables: wff setvar class
This definition is referenced by:  isirred  18745
  Copyright terms: Public domain W3C validator