Definition df-rgspn 20870

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

Step	Hyp	Ref	Expression
1		crgspn 20869	. 2 class RingSpan
2		vw	. . 3 setvar 𝑤
3		cvv 3450	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1568	. . . . . 6 class 𝑤
6		cbs 17394	. . . . . 6 class Base
7	5, 6	cfv 6541	. . . . 5 class (Base‘𝑤)
8	7	cpw 4556	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1568	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1568	. . . . . . 7 class 𝑡
12	9, 11	wss 3896	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		csubrg 20828	. . . . . . 7 class SubRing
14	5, 13	cfv 6541	. . . . . 6 class (SubRing‘𝑤)
15	12, 10, 14	crab 3412	. . . . 5 class {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
16	15	cint 4906	. . . 4 class ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
17	4, 8, 16	cmpt 5185	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})
18	2, 3, 17	cmpt 5185	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
19	1, 18	wceq 1569	1 wff RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

This definition is used by:  rgspnval  20871