Definition df-asp 19313

Description: Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
df-asp	|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )

Distinct variable group:   t, s, w

Detailed syntax breakdown of Definition df-asp

Step	Hyp	Ref	Expression
1		casp 19310	. 2 class AlgSpan
2		vw	. . 3 setvar w
3		casa 19309	. . 3 class AssAlg
4		vs	. . . 4 setvar s
5	2	cv 1482	. . . . . 6 class w
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` w )
8	7	cpw 4158	. . . 4 class ~P ( Base ` w )
9	4	cv 1482	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1482	. . . . . . 7 class t
12	9, 11	wss 3574	. . . . . 6 wff s C_ t
13		csubrg 18776	. . . . . . . 8 class SubRing
14	5, 13	cfv 5888	. . . . . . 7 class (SubRing ` w )
15		clss 18932	. . . . . . . 8 class LSubSp
16	5, 15	cfv 5888	. . . . . . 7 class ( LSubSp ` w )
17	14, 16	cin 3573	. . . . . 6 class ( (SubRing ` w ) i^i ( LSubSp ` w ) )
18	12, 10, 17	crab 2916	. . . . 5 class { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t }
19	18	cint 4475	. . . 4 class |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t }
20	4, 8, 19	cmpt 4729	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } )
21	2, 3, 20	cmpt 4729	. 2 class ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
22	1, 21	wceq 1483	1 wff AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )

This definition is referenced by:  aspval  19328