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

Definition df-irred 16757
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 16754 . 2  class Irred
2 vw . . 3  setvar  w
3 cvv 2993 . . 3  class  _V
4 vb . . . 4  setvar  b
52cv 1368 . . . . . 6  class  w
6 cbs 14195 . . . . . 6  class  Base
75, 6cfv 5439 . . . . 5  class  ( Base `  w )
8 cui 16753 . . . . . 6  class Unit
95, 8cfv 5439 . . . . 5  class  (Unit `  w )
107, 9cdif 3346 . . . 4  class  ( (
Base `  w )  \  (Unit `  w )
)
11 vx . . . . . . . . . 10  setvar  x
1211cv 1368 . . . . . . . . 9  class  x
13 vy . . . . . . . . . 10  setvar  y
1413cv 1368 . . . . . . . . 9  class  y
15 cmulr 14260 . . . . . . . . . 10  class  .r
165, 15cfv 5439 . . . . . . . . 9  class  ( .r
`  w )
1712, 14, 16co 6112 . . . . . . . 8  class  ( x ( .r `  w
) y )
18 vz . . . . . . . . 9  setvar  z
1918cv 1368 . . . . . . . 8  class  z
2017, 19wne 2620 . . . . . . 7  wff  ( x ( .r `  w
) y )  =/=  z
214cv 1368 . . . . . . 7  class  b
2220, 13, 21wral 2736 . . . . . 6  wff  A. y  e.  b  ( x
( .r `  w
) y )  =/=  z
2322, 11, 21wral 2736 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( x
( .r `  w
) y )  =/=  z
2423, 18, 21crab 2740 . . . 4  class  { z  e.  b  |  A. x  e.  b  A. y  e.  b  (
x ( .r `  w ) y )  =/=  z }
254, 10, 24csb 3309 . . 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 4371 . 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 1369 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 setvar class
This definition is referenced by:  isirred  16813
  Copyright terms: Public domain W3C validator