df-idl - Mathbox for Jeff Madsen

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

Definition df-idl 38017

Description: Define the class of (two-sided) ideals of a ring 𝑅. A subset of 𝑅 is an ideal if it contains 0, 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	⊢ Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1^st ‘𝑟) ∣ ((GId‘(1^st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)))})

Distinct variable group: 𝑖,𝑟,𝑥,𝑦,𝑧

**Detailed syntax breakdown of Definition df-idl**
Step	Hyp	Ref	Expression
1		cidl 38014	. 2 class Idl
2		vr	. . 3 setvar 𝑟
3		crngo 37901	. . 3 class RingOps
4	2	cv 1539	. . . . . . . 8 class 𝑟
5		c1st 8012	. . . . . . . 8 class 1^st
6	4, 5	cfv 6561	. . . . . . 7 class (1^st ‘𝑟)
7		cgi 30509	. . . . . . 7 class GId
8	6, 7	cfv 6561	. . . . . 6 class (GId‘(1^st ‘𝑟))
9		vi	. . . . . . 7 setvar 𝑖
10	9	cv 1539	. . . . . 6 class 𝑖
11	8, 10	wcel 2108	. . . . 5 wff (GId‘(1^st ‘𝑟)) ∈ 𝑖
12		vx	. . . . . . . . . . 11 setvar 𝑥
13	12	cv 1539	. . . . . . . . . 10 class 𝑥
14		vy	. . . . . . . . . . 11 setvar 𝑦
15	14	cv 1539	. . . . . . . . . 10 class 𝑦
16	13, 15, 6	co 7431	. . . . . . . . 9 class (𝑥(1^st ‘𝑟)𝑦)
17	16, 10	wcel 2108	. . . . . . . 8 wff (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖
18	17, 14, 10	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖
19		vz	. . . . . . . . . . . 12 setvar 𝑧
20	19	cv 1539	. . . . . . . . . . 11 class 𝑧
21		c2nd 8013	. . . . . . . . . . . 12 class 2^nd
22	4, 21	cfv 6561	. . . . . . . . . . 11 class (2^nd ‘𝑟)
23	20, 13, 22	co 7431	. . . . . . . . . 10 class (𝑧(2^nd ‘𝑟)𝑥)
24	23, 10	wcel 2108	. . . . . . . . 9 wff (𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖
25	13, 20, 22	co 7431	. . . . . . . . . 10 class (𝑥(2^nd ‘𝑟)𝑧)
26	25, 10	wcel 2108	. . . . . . . . 9 wff (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖
27	24, 26	wa 395	. . . . . . . 8 wff ((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)
28	6	crn 5686	. . . . . . . 8 class ran (1^st ‘𝑟)
29	27, 19, 28	wral 3061	. . . . . . 7 wff ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)
30	18, 29	wa 395	. . . . . 6 wff (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖))
31	30, 12, 10	wral 3061	. . . . 5 wff ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖))
32	11, 31	wa 395	. . . 4 wff ((GId‘(1^st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)))
33	28	cpw 4600	. . . 4 class 𝒫 ran (1^st ‘𝑟)
34	32, 9, 33	crab 3436	. . 3 class {𝑖 ∈ 𝒫 ran (1^st ‘𝑟) ∣ ((GId‘(1^st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)))}
35	2, 3, 34	cmpt 5225	. 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1^st ‘𝑟) ∣ ((GId‘(1^st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)))})
36	1, 35	wceq 1540	1 wff Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1^st ‘𝑟) ∣ ((GId‘(1^st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1^st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1^st ‘𝑟)((𝑧(2^nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2^nd ‘𝑟)𝑧) ∈ 𝑖)))})

Colors of variables: wff setvar class

This definition is referenced by: idlval 38020

W3C validator