Metamath Proof Explorer

Definition df-irred

Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Assertion 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 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cir 
 |-  Irred
1 vw 
 |-  w
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 1 cv 
 |-  w
5 4 3 cfv 
 |-  ( Base ` w )
6 cui 
 |-  Unit
7 4 6 cfv 
 |-  ( Unit ` w )
8 5 7 cdif 
 |-  ( ( Base ` w ) \ ( Unit ` w ) )
9 vb 
 |-  b
10 vz 
 |-  z
11 9 cv 
 |-  b
12 vx 
 |-  x
13 vy 
 |-  y
14 12 cv 
 |-  x
15 cmulr 
 |-  .r
16 4 15 cfv 
 |-  ( .r ` w )
17 13 cv 
 |-  y
18 14 17 16 co 
 |-  ( x ( .r ` w ) y )
19 10 cv 
 |-  z
20 18 19 wne 
 |-  ( x ( .r ` w ) y ) =/= z
21 20 13 11 wral 
 |-  A. y e. b ( x ( .r ` w ) y ) =/= z
22 21 12 11 wral 
 |-  A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z
23 22 10 11 crab 
 |-  { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z }
24 9 8 23 csb 
 |-  [_ ( ( Base ` w ) \ ( Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z }
25 1 2 24 cmpt 
 |-  ( w e. _V |-> [_ ( ( Base ` w ) \ ( Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
26 0 25 wceq 
 |-  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 } )