# Metamath Proof Explorer

## 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 ${⊢}\mathrm{RingSpan}=\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crgspn ${class}\mathrm{RingSpan}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{w}}$
8 vt ${setvar}{t}$
9 csubrg ${class}\mathrm{SubRing}$
10 5 9 cfv ${class}\mathrm{SubRing}\left({w}\right)$
11 3 cv ${setvar}{s}$
12 8 cv ${setvar}{t}$
13 11 12 wss ${wff}{s}\subseteq {t}$
14 13 8 10 crab ${class}\left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}$
15 14 cint ${class}\bigcap \left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}$
16 3 7 15 cmpt ${class}\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}\right)$
17 1 2 16 cmpt ${class}\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$
18 0 17 wceq ${wff}\mathrm{RingSpan}=\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{SubRing}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$