Definition df-lsp

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clspn	|- LSpan
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		clss	|- LSubSp
10	5 9	cfv	|- ( LSubSp ` w )
11	3	cv	|- s
12	8	cv	|- t
13	11 12	wss	|- s C_ t
14	13 8 10	crab	|- { t e. ( LSubSp ` w ) | s C_ t }
15	14	cint	|- |^| { t e. ( LSubSp ` w ) | s C_ t }
16	3 7 15	cmpt	|- ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } )
17	1 2 16	cmpt	|- ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
18	0 17	wceq	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )