Metamath Proof Explorer

Definition df-idl

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidl 
 |-  Idl
1 vr 
 |-  r
2 crngo 
 |-  RingOps
3 vi 
 |-  i
4 c1st 
 |-  1st
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( 1st ` r )
7 6 crn 
 |-  ran ( 1st ` r )
8 7 cpw 
 |-  ~P ran ( 1st ` r )
9 cgi 
 |-  GId
10 6 9 cfv 
 |-  ( GId ` ( 1st ` r ) )
11 3 cv 
 |-  i
12 10 11 wcel 
 |-  ( GId ` ( 1st ` r ) ) e. i
13 vx 
 |-  x
14 vy 
 |-  y
15 13 cv 
 |-  x
16 14 cv 
 |-  y
17 15 16 6 co 
 |-  ( x ( 1st ` r ) y )
18 17 11 wcel 
 |-  ( x ( 1st ` r ) y ) e. i
19 18 14 11 wral 
 |-  A. y e. i ( x ( 1st ` r ) y ) e. i
20 vz 
 |-  z
21 20 cv 
 |-  z
22 c2nd 
 |-  2nd
23 5 22 cfv 
 |-  ( 2nd ` r )
24 21 15 23 co 
 |-  ( z ( 2nd ` r ) x )
25 24 11 wcel 
 |-  ( z ( 2nd ` r ) x ) e. i
26 15 21 23 co 
 |-  ( x ( 2nd ` r ) z )
27 26 11 wcel 
 |-  ( x ( 2nd ` r ) z ) e. i
28 25 27 wa 
 |-  ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i )
29 28 20 7 wral 
 |-  A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i )
30 19 29 wa 
 |-  ( 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 ) )
31 30 13 11 wral 
 |-  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 ) )
32 12 31 wa 
 |-  ( ( 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 ) ) )
33 32 3 8 crab 
 |-  { 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 ) ) ) }
34 1 2 33 cmpt 
 |-  ( 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 ) ) ) } )
35 0 34 wceq 
 |-  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 ) ) ) } )