Definition df-rgspn

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)

	Ref	Expression
Assertion	df-rgspn	⊢ RingSpan = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crgspn	⊢ RingSpan
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		vt	⊢ 𝑡
9		csubrg	⊢ SubRing
10	5 9	cfv	⊢ ( SubRing ‘ 𝑤 )
11	3	cv	⊢ 𝑠
12	8	cv	⊢ 𝑡
13	11 12	wss	⊢ 𝑠 ⊆ 𝑡
14	13 8 10	crab	⊢ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 }
15	14	cint	⊢ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 }
16	3 7 15	cmpt	⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } )
17	1 2 16	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )
18	0 17	wceq	⊢ RingSpan = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )