Definition df-idl 33809

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

Step	Hyp	Ref	Expression
1		cidl 33806	. 2 class Idl
2		vr	. . 3 setvar r
3		crngo 33693	. . 3 class RingOps
4	2	cv 1482	. . . . . . . 8 class r
5		c1st 7166	. . . . . . . 8 class 1st
6	4, 5	cfv 5888	. . . . . . 7 class ( 1st ` r )
7		cgi 27344	. . . . . . 7 class GId
8	6, 7	cfv 5888	. . . . . 6 class (GId ` ( 1st ` r ) )
9		vi	. . . . . . 7 setvar i
10	9	cv 1482	. . . . . 6 class i
11	8, 10	wcel 1990	. . . . 5 wff (GId ` ( 1st ` r ) ) e. i
12		vx	. . . . . . . . . . 11 setvar x
13	12	cv 1482	. . . . . . . . . 10 class x
14		vy	. . . . . . . . . . 11 setvar y
15	14	cv 1482	. . . . . . . . . 10 class y
16	13, 15, 6	co 6650	. . . . . . . . 9 class ( x ( 1st ` r ) y )
17	16, 10	wcel 1990	. . . . . . . 8 wff ( x ( 1st ` r ) y ) e. i
18	17, 14, 10	wral 2912	. . . . . . 7 wff A. y e. i ( x ( 1st ` r ) y ) e. i
19		vz	. . . . . . . . . . . 12 setvar z
20	19	cv 1482	. . . . . . . . . . 11 class z
21		c2nd 7167	. . . . . . . . . . . 12 class 2nd
22	4, 21	cfv 5888	. . . . . . . . . . 11 class ( 2nd ` r )
23	20, 13, 22	co 6650	. . . . . . . . . 10 class ( z ( 2nd ` r ) x )
24	23, 10	wcel 1990	. . . . . . . . 9 wff ( z ( 2nd ` r ) x ) e. i
25	13, 20, 22	co 6650	. . . . . . . . . 10 class ( x ( 2nd ` r ) z )
26	25, 10	wcel 1990	. . . . . . . . 9 wff ( x ( 2nd ` r ) z ) e. i
27	24, 26	wa 384	. . . . . . . 8 wff ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i )
28	6	crn 5115	. . . . . . . 8 class ran ( 1st ` r )
29	27, 19, 28	wral 2912	. . . . . . 7 wff A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i )
30	18, 29	wa 384	. . . . . 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 ) )
31	30, 12, 10	wral 2912	. . . . 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 ) )
32	11, 31	wa 384	. . . 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 ) ) )
33	28	cpw 4158	. . . 4 class ~P ran ( 1st ` r )
34	32, 9, 33	crab 2916	. . 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 ) ) ) }
35	2, 3, 34	cmpt 4729	. 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 ) ) ) } )
36	1, 35	wceq 1483	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 ) ) ) } )

This definition is referenced by:  idlval  33812