Metamath Proof Explorer


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 } ) )