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 34140
 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 (1st𝑟) ∣ ((GId‘(1st𝑟)) ∈ 𝑖 ∧ ∀𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)))})
Distinct variable group:   𝑖,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-idl
StepHypRef Expression
1 cidl 34137 . 2 class Idl
2 vr . . 3 setvar 𝑟
3 crngo 34024 . . 3 class RingOps
42cv 1631 . . . . . . . 8 class 𝑟
5 c1st 7332 . . . . . . . 8 class 1st
64, 5cfv 6049 . . . . . . 7 class (1st𝑟)
7 cgi 27674 . . . . . . 7 class GId
86, 7cfv 6049 . . . . . 6 class (GId‘(1st𝑟))
9 vi . . . . . . 7 setvar 𝑖
109cv 1631 . . . . . 6 class 𝑖
118, 10wcel 2139 . . . . 5 wff (GId‘(1st𝑟)) ∈ 𝑖
12 vx . . . . . . . . . . 11 setvar 𝑥
1312cv 1631 . . . . . . . . . 10 class 𝑥
14 vy . . . . . . . . . . 11 setvar 𝑦
1514cv 1631 . . . . . . . . . 10 class 𝑦
1613, 15, 6co 6814 . . . . . . . . 9 class (𝑥(1st𝑟)𝑦)
1716, 10wcel 2139 . . . . . . . 8 wff (𝑥(1st𝑟)𝑦) ∈ 𝑖
1817, 14, 10wral 3050 . . . . . . 7 wff 𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖
19 vz . . . . . . . . . . . 12 setvar 𝑧
2019cv 1631 . . . . . . . . . . 11 class 𝑧
21 c2nd 7333 . . . . . . . . . . . 12 class 2nd
224, 21cfv 6049 . . . . . . . . . . 11 class (2nd𝑟)
2320, 13, 22co 6814 . . . . . . . . . 10 class (𝑧(2nd𝑟)𝑥)
2423, 10wcel 2139 . . . . . . . . 9 wff (𝑧(2nd𝑟)𝑥) ∈ 𝑖
2513, 20, 22co 6814 . . . . . . . . . 10 class (𝑥(2nd𝑟)𝑧)
2625, 10wcel 2139 . . . . . . . . 9 wff (𝑥(2nd𝑟)𝑧) ∈ 𝑖
2724, 26wa 383 . . . . . . . 8 wff ((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)
286crn 5267 . . . . . . . 8 class ran (1st𝑟)
2927, 19, 28wral 3050 . . . . . . 7 wff 𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)
3018, 29wa 383 . . . . . 6 wff (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖))
3130, 12, 10wral 3050 . . . . 5 wff 𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖))
3211, 31wa 383 . . . 4 wff ((GId‘(1st𝑟)) ∈ 𝑖 ∧ ∀𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)))
3328cpw 4302 . . . 4 class 𝒫 ran (1st𝑟)
3432, 9, 33crab 3054 . . 3 class {𝑖 ∈ 𝒫 ran (1st𝑟) ∣ ((GId‘(1st𝑟)) ∈ 𝑖 ∧ ∀𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)))}
352, 3, 34cmpt 4881 . 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1st𝑟) ∣ ((GId‘(1st𝑟)) ∈ 𝑖 ∧ ∀𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)))})
361, 35wceq 1632 1 wff Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1st𝑟) ∣ ((GId‘(1st𝑟)) ∈ 𝑖 ∧ ∀𝑥𝑖 (∀𝑦𝑖 (𝑥(1st𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st𝑟)((𝑧(2nd𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd𝑟)𝑧) ∈ 𝑖)))})
 Colors of variables: wff setvar class This definition is referenced by:  idlval  34143
 Copyright terms: Public domain W3C validator