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

Definition df-idl 26634
 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 26631 . 2
2 vr . . 3
3 crngo 21968 . . 3
42cv 1652 . . . . . . . 8
5 c1st 6350 . . . . . . . 8
64, 5cfv 5457 . . . . . . 7
7 cgi 21780 . . . . . . 7 GId
86, 7cfv 5457 . . . . . 6 GId
9 vi . . . . . . 7
109cv 1652 . . . . . 6
118, 10wcel 1726 . . . . 5 GId
12 vx . . . . . . . . . . 11
1312cv 1652 . . . . . . . . . 10
14 vy . . . . . . . . . . 11
1514cv 1652 . . . . . . . . . 10
1613, 15, 6co 6084 . . . . . . . . 9
1716, 10wcel 1726 . . . . . . . 8
1817, 14, 10wral 2707 . . . . . . 7
19 vz . . . . . . . . . . . 12
2019cv 1652 . . . . . . . . . . 11
21 c2nd 6351 . . . . . . . . . . . 12
224, 21cfv 5457 . . . . . . . . . . 11
2320, 13, 22co 6084 . . . . . . . . . 10
2423, 10wcel 1726 . . . . . . . . 9
2513, 20, 22co 6084 . . . . . . . . . 10
2625, 10wcel 1726 . . . . . . . . 9
2724, 26wa 360 . . . . . . . 8
286crn 4882 . . . . . . . 8
2927, 19, 28wral 2707 . . . . . . 7
3018, 29wa 360 . . . . . 6
3130, 12, 10wral 2707 . . . . 5
3211, 31wa 360 . . . 4 GId
3328cpw 3801 . . . 4
3432, 9, 33crab 2711 . . 3 GId
352, 3, 34cmpt 4269 . 2 GId
361, 35wceq 1653 1 GId
 Colors of variables: wff set class This definition is referenced by:  idlval  26637
 Copyright terms: Public domain W3C validator