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

Definition df-igen 34190
Description: Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-igen IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st𝑟) ↦ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠𝑗})
Distinct variable group:   𝑠,𝑟,𝑗

Detailed syntax breakdown of Definition df-igen
StepHypRef Expression
1 cigen 34189 . 2 class IdlGen
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 34024 . . 3 class RingOps
52cv 1631 . . . . . 6 class 𝑟
6 c1st 7332 . . . . . 6 class 1st
75, 6cfv 6049 . . . . 5 class (1st𝑟)
87crn 5267 . . . 4 class ran (1st𝑟)
98cpw 4302 . . 3 class 𝒫 ran (1st𝑟)
103cv 1631 . . . . . 6 class 𝑠
11 vj . . . . . . 7 setvar 𝑗
1211cv 1631 . . . . . 6 class 𝑗
1310, 12wss 3715 . . . . 5 wff 𝑠𝑗
14 cidl 34137 . . . . . 6 class Idl
155, 14cfv 6049 . . . . 5 class (Idl‘𝑟)
1613, 11, 15crab 3054 . . . 4 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠𝑗}
1716cint 4627 . . 3 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠𝑗}
182, 3, 4, 9, 17cmpt2 6816 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st𝑟) ↦ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠𝑗})
191, 18wceq 1632 1 wff IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st𝑟) ↦ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  igenval  34191
  Copyright terms: Public domain W3C validator