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

Definition df-irred 15425
Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
Assertion
Ref Expression
df-irred  |- Irred  =  ( w  e.  _V  |->  [_ ( ( Base `  w
)  \  (Unit `  w
) )  /  b ]_ { z  e.  b  |  A. x  e.  b  A. y  e.  b  ( x ( .r `  w ) y )  =/=  z } )
Distinct variable group:    w, b, x, y, z

Detailed syntax breakdown of Definition df-irred
StepHypRef Expression
1 cir 15422 . 2  class Irred
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1622 . . . . . 6  class  w
6 cbs 13148 . . . . . 6  class  Base
75, 6cfv 5255 . . . . 5  class  ( Base `  w )
8 cui 15421 . . . . . 6  class Unit
95, 8cfv 5255 . . . . 5  class  (Unit `  w )
107, 9cdif 3149 . . . 4  class  ( (
Base `  w )  \  (Unit `  w )
)
11 vx . . . . . . . . . 10  set  x
1211cv 1622 . . . . . . . . 9  class  x
13 vy . . . . . . . . . 10  set  y
1413cv 1622 . . . . . . . . 9  class  y
15 cmulr 13209 . . . . . . . . . 10  class  .r
165, 15cfv 5255 . . . . . . . . 9  class  ( .r
`  w )
1712, 14, 16co 5858 . . . . . . . 8  class  ( x ( .r `  w
) y )
18 vz . . . . . . . . 9  set  z
1918cv 1622 . . . . . . . 8  class  z
2017, 19wne 2446 . . . . . . 7  wff  ( x ( .r `  w
) y )  =/=  z
214cv 1622 . . . . . . 7  class  b
2220, 13, 21wral 2543 . . . . . 6  wff  A. y  e.  b  ( x
( .r `  w
) y )  =/=  z
2322, 11, 21wral 2543 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( x
( .r `  w
) y )  =/=  z
2423, 18, 21crab 2547 . . . 4  class  { z  e.  b  |  A. x  e.  b  A. y  e.  b  (
x ( .r `  w ) y )  =/=  z }
254, 10, 24csb 3081 . . 3  class  [_ (
( Base `  w )  \  (Unit `  w )
)  /  b ]_ { z  e.  b  |  A. x  e.  b  A. y  e.  b  ( x ( .r `  w ) y )  =/=  z }
262, 3, 25cmpt 4077 . 2  class  ( w  e.  _V  |->  [_ (
( Base `  w )  \  (Unit `  w )
)  /  b ]_ { z  e.  b  |  A. x  e.  b  A. y  e.  b  ( x ( .r `  w ) y )  =/=  z } )
271, 26wceq 1623 1  wff Irred  =  ( w  e.  _V  |->  [_ ( ( Base `  w
)  \  (Unit `  w
) )  /  b ]_ { z  e.  b  |  A. x  e.  b  A. y  e.  b  ( x ( .r `  w ) y )  =/=  z } )
Colors of variables: wff set class
This definition is referenced by:  isirred  15481
  Copyright terms: Public domain W3C validator