Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-idlNEW Unicode version

Definition df-idlNEW 25547
 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.) (Revised by FL, 29-Oct-2014.)
Assertion
Ref Expression
df-idlNEW IdlNEW
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-idlNEW
StepHypRef Expression
1 cidln 25546 . 2 IdlNEW
2 vr . . 3
3 crg 15353 . . 3
42cv 1631 . . . . . . 7
5 c0g 13416 . . . . . . 7
64, 5cfv 5271 . . . . . 6
7 vi . . . . . . 7
87cv 1631 . . . . . 6
96, 8wcel 1696 . . . . 5
10 vx . . . . . . . . . . 11
1110cv 1631 . . . . . . . . . 10
12 vy . . . . . . . . . . 11
1312cv 1631 . . . . . . . . . 10
14 cplusg 13224 . . . . . . . . . . 11
154, 14cfv 5271 . . . . . . . . . 10
1611, 13, 15co 5874 . . . . . . . . 9
1716, 8wcel 1696 . . . . . . . 8
1817, 12, 8wral 2556 . . . . . . 7
19 vz . . . . . . . . . . . 12
2019cv 1631 . . . . . . . . . . 11
21 cmulr 13225 . . . . . . . . . . . 12
224, 21cfv 5271 . . . . . . . . . . 11
2320, 11, 22co 5874 . . . . . . . . . 10
2423, 8wcel 1696 . . . . . . . . 9
2511, 20, 22co 5874 . . . . . . . . . 10
2625, 8wcel 1696 . . . . . . . . 9
2724, 26wa 358 . . . . . . . 8
28 cbs 13164 . . . . . . . . 9
294, 28cfv 5271 . . . . . . . 8
3027, 19, 29wral 2556 . . . . . . 7
3118, 30wa 358 . . . . . 6
3231, 10, 8wral 2556 . . . . 5
339, 32wa 358 . . . 4
3429cpw 3638 . . . 4
3533, 7, 34crab 2560 . . 3
362, 3, 35cmpt 4093 . 2
371, 36wceq 1632 1 IdlNEW
 Colors of variables: wff set class This definition is referenced by:  idlvalNEW  25548
 Copyright terms: Public domain W3C validator