Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-idl Unicode version

Definition df-idl 26635
Description: Define the class of (two-sided) ideals of a ring  R. A subset of  R is an ideal if it contains  0, is closed under addition, and is closed under multiplication on either side by any element of  R. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-idl  |-  Idl  =  ( r  e.  RingOps  |->  { i  e.  ~P ran  ( 1st `  r )  |  ( (GId `  ( 1st `  r ) )  e.  i  /\  A. x  e.  i  ( A. y  e.  i  ( x ( 1st `  r ) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r ) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) ) ) } )
Distinct variable group:    i, r, x, y, z

Detailed syntax breakdown of Definition df-idl
StepHypRef Expression
1 cidl 26632 . 2  class  Idl
2 vr . . 3  set  r
3 crngo 21042 . . 3  class  RingOps
42cv 1622 . . . . . . . 8  class  r
5 c1st 6120 . . . . . . . 8  class  1st
64, 5cfv 5255 . . . . . . 7  class  ( 1st `  r )
7 cgi 20854 . . . . . . 7  class GId
86, 7cfv 5255 . . . . . 6  class  (GId `  ( 1st `  r ) )
9 vi . . . . . . 7  set  i
109cv 1622 . . . . . 6  class  i
118, 10wcel 1684 . . . . 5  wff  (GId `  ( 1st `  r ) )  e.  i
12 vx . . . . . . . . . . 11  set  x
1312cv 1622 . . . . . . . . . 10  class  x
14 vy . . . . . . . . . . 11  set  y
1514cv 1622 . . . . . . . . . 10  class  y
1613, 15, 6co 5858 . . . . . . . . 9  class  ( x ( 1st `  r
) y )
1716, 10wcel 1684 . . . . . . . 8  wff  ( x ( 1st `  r
) y )  e.  i
1817, 14, 10wral 2543 . . . . . . 7  wff  A. y  e.  i  ( x
( 1st `  r
) y )  e.  i
19 vz . . . . . . . . . . . 12  set  z
2019cv 1622 . . . . . . . . . . 11  class  z
21 c2nd 6121 . . . . . . . . . . . 12  class  2nd
224, 21cfv 5255 . . . . . . . . . . 11  class  ( 2nd `  r )
2320, 13, 22co 5858 . . . . . . . . . 10  class  ( z ( 2nd `  r
) x )
2423, 10wcel 1684 . . . . . . . . 9  wff  ( z ( 2nd `  r
) x )  e.  i
2513, 20, 22co 5858 . . . . . . . . . 10  class  ( x ( 2nd `  r
) z )
2625, 10wcel 1684 . . . . . . . . 9  wff  ( x ( 2nd `  r
) z )  e.  i
2724, 26wa 358 . . . . . . . 8  wff  ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i )
286crn 4690 . . . . . . . 8  class  ran  ( 1st `  r )
2927, 19, 28wral 2543 . . . . . . 7  wff  A. z  e.  ran  ( 1st `  r
) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i )
3018, 29wa 358 . . . . . 6  wff  ( A. y  e.  i  (
x ( 1st `  r
) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r
) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) )
3130, 12, 10wral 2543 . . . . 5  wff  A. x  e.  i  ( A. y  e.  i  (
x ( 1st `  r
) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r
) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) )
3211, 31wa 358 . . . 4  wff  ( (GId
`  ( 1st `  r
) )  e.  i  /\  A. x  e.  i  ( A. y  e.  i  ( x
( 1st `  r
) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r
) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) ) )
3328cpw 3625 . . . 4  class  ~P ran  ( 1st `  r )
3432, 9, 33crab 2547 . . 3  class  { i  e.  ~P ran  ( 1st `  r )  |  ( (GId `  ( 1st `  r ) )  e.  i  /\  A. x  e.  i  ( A. y  e.  i 
( x ( 1st `  r ) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r ) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) ) ) }
352, 3, 34cmpt 4077 . 2  class  ( r  e.  RingOps  |->  { i  e. 
~P ran  ( 1st `  r )  |  ( (GId `  ( 1st `  r ) )  e.  i  /\  A. x  e.  i  ( A. y  e.  i  (
x ( 1st `  r
) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r
) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) ) ) } )
361, 35wceq 1623 1  wff  Idl  =  ( r  e.  RingOps  |->  { i  e.  ~P ran  ( 1st `  r )  |  ( (GId `  ( 1st `  r ) )  e.  i  /\  A. x  e.  i  ( A. y  e.  i  ( x ( 1st `  r ) y )  e.  i  /\  A. z  e.  ran  ( 1st `  r ) ( ( z ( 2nd `  r
) x )  e.  i  /\  ( x ( 2nd `  r
) z )  e.  i ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  idlval  26638
  Copyright terms: Public domain W3C validator