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

Definition df-idl 31958
 Description: Define the class of (two-sided) ideals of a ring . A subset of is an ideal if it contains , is closed under addition, and is closed under multiplication on either side by any element of . (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-idl GId
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-idl
StepHypRef Expression
1 cidl 31955 . 2
2 vr . . 3
3 crngo 25956 . . 3
42cv 1436 . . . . . . . 8
5 c1st 6805 . . . . . . . 8
64, 5cfv 5601 . . . . . . 7
7 cgi 25768 . . . . . . 7 GId
86, 7cfv 5601 . . . . . 6 GId
9 vi . . . . . . 7
109cv 1436 . . . . . 6
118, 10wcel 1870 . . . . 5 GId
12 vx . . . . . . . . . . 11
1312cv 1436 . . . . . . . . . 10
14 vy . . . . . . . . . . 11
1514cv 1436 . . . . . . . . . 10
1613, 15, 6co 6305 . . . . . . . . 9
1716, 10wcel 1870 . . . . . . . 8
1817, 14, 10wral 2782 . . . . . . 7
19 vz . . . . . . . . . . . 12
2019cv 1436 . . . . . . . . . . 11
21 c2nd 6806 . . . . . . . . . . . 12
224, 21cfv 5601 . . . . . . . . . . 11
2320, 13, 22co 6305 . . . . . . . . . 10
2423, 10wcel 1870 . . . . . . . . 9
2513, 20, 22co 6305 . . . . . . . . . 10
2625, 10wcel 1870 . . . . . . . . 9
2724, 26wa 370 . . . . . . . 8
286crn 4855 . . . . . . . 8
2927, 19, 28wral 2782 . . . . . . 7
3018, 29wa 370 . . . . . 6
3130, 12, 10wral 2782 . . . . 5
3211, 31wa 370 . . . 4 GId
3328cpw 3985 . . . 4
3432, 9, 33crab 2786 . . 3 GId
352, 3, 34cmpt 4484 . 2 GId
361, 35wceq 1437 1 GId
 Colors of variables: wff setvar class This definition is referenced by:  idlval  31961
 Copyright terms: Public domain W3C validator