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