Definition df-lsp 13539

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 13538	. 2 class LSpan
2		vw	. . 3 setvar w
3		cvv 2749	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1362	. . . . . 6 class w
6		cbs 12475	. . . . . 6 class Base
7	5, 6	cfv 5228	. . . . 5 class ( Base ` w )
8	7	cpw 3587	. . . 4 class ~P ( Base ` w )
9	4	cv 1362	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1362	. . . . . . 7 class t
12	9, 11	wss 3141	. . . . . 6 wff s C_ t
13		clss 13504	. . . . . . 7 class LSubSp
14	5, 13	cfv 5228	. . . . . 6 class ( LSubSp ` w )
15	12, 10, 14	crab 2469	. . . . 5 class { t e. ( LSubSp ` w ) | s C_ t }
16	15	cint 3856	. . . 4 class |^| { t e. ( LSubSp ` w ) | s C_ t }
17	4, 8, 16	cmpt 4076	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } )
18	2, 3, 17	cmpt 4076	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
19	1, 18	wceq 1363	1 wff LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )

This definition is referenced by:  lspfval  13540