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 = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( SubRing ` w ) | s C_ t } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crgspn	|- RingSpan
1		vw	|- w
2		cvv	|- _V
3		vs	|- s
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7	6	cpw	|- ~P ( Base ` w )
8		vt	|- t
9		csubrg	|- SubRing
10	5 9	cfv	|- ( SubRing ` w )
11	3	cv	|- s
12	8	cv	|- t
13	11 12	wss	|- s C_ t
14	13 8 10	crab	|- { t e. ( SubRing ` w ) | s C_ t }
15	14	cint	|- |^| { t e. ( SubRing ` w ) | s C_ t }
16	3 7 15	cmpt	|- ( s e. ~P ( Base ` w ) |-> |^| { t e. ( SubRing ` w ) | s C_ t } )
17	1 2 16	cmpt	|- ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( SubRing ` w ) | s C_ t } ) )
18	0 17	wceq	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( SubRing ` w ) | s C_ t } ) )