ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rgspn GIF version

Definition df-rgspn 13404
Description: The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)
Assertion
Ref Expression
df-rgspn RingSpan = (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
Distinct variable group:   𝑀,𝑠,𝑑

Detailed syntax breakdown of Definition df-rgspn
StepHypRef Expression
1 crgspn 13402 . 2 class RingSpan
2 vw . . 3 setvar 𝑀
3 cvv 2749 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1362 . . . . . 6 class 𝑀
6 cbs 12475 . . . . . 6 class Base
75, 6cfv 5228 . . . . 5 class (Baseβ€˜π‘€)
87cpw 3587 . . . 4 class 𝒫 (Baseβ€˜π‘€)
94cv 1362 . . . . . . 7 class 𝑠
10 vt . . . . . . . 8 setvar 𝑑
1110cv 1362 . . . . . . 7 class 𝑑
129, 11wss 3141 . . . . . 6 wff 𝑠 βŠ† 𝑑
13 csubrg 13401 . . . . . . 7 class SubRing
145, 13cfv 5228 . . . . . 6 class (SubRingβ€˜π‘€)
1512, 10, 14crab 2469 . . . . 5 class {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}
1615cint 3856 . . . 4 class ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}
174, 8, 16cmpt 4076 . . 3 class (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑})
182, 3, 17cmpt 4076 . 2 class (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
191, 18wceq 1363 1 wff RingSpan = (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
Colors of variables: wff set class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator