Definition df-lsp 14149

Description: Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)

Assertion

Ref	Expression
df-lsp	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )

Distinct variable group:   w, s, t

Detailed syntax breakdown of Definition df-lsp

Step	Hyp	Ref	Expression
1		clspn 14148	. 2 class LSpan
2		vw	. . 3 setvar w
3		cvv 2772	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1372	. . . . . 6 class w
6		cbs 12832	. . . . . 6 class Base
7	5, 6	cfv 5271	. . . . 5 class ( Base ` w )
8	7	cpw 3616	. . . 4 class ~P ( Base ` w )
9	4	cv 1372	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1372	. . . . . . 7 class t
12	9, 11	wss 3166	. . . . . 6 wff s C_ t
13		clss 14114	. . . . . . 7 class LSubSp
14	5, 13	cfv 5271	. . . . . 6 class ( LSubSp ` w )
15	12, 10, 14	crab 2488	. . . . 5 class { t e. ( LSubSp ` w ) | s C_ t }
16	15	cint 3885	. . . 4 class |^| { t e. ( LSubSp ` w ) | s C_ t }
17	4, 8, 16	cmpt 4105	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } )
18	2, 3, 17	cmpt 4105	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
19	1, 18	wceq 1373	1 wff LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )

This definition is referenced by:  lspfval  14150