# 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 ${⊢}\mathrm{LSpan}=\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clspn ${class}\mathrm{LSpan}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{w}}$
8 vt ${setvar}{t}$
9 clss ${class}\mathrm{LSubSp}$
10 5 9 cfv ${class}\mathrm{LSubSp}\left({w}\right)$
11 3 cv ${setvar}{s}$
12 8 cv ${setvar}{t}$
13 11 12 wss ${wff}{s}\subseteq {t}$
14 13 8 10 crab ${class}\left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}$
15 14 cint ${class}\bigcap \left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}$
16 3 7 15 cmpt ${class}\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}\right)$
17 1 2 16 cmpt ${class}\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$
18 0 17 wceq ${wff}\mathrm{LSpan}=\left({w}\in \mathrm{V}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \mathrm{LSubSp}\left({w}\right)|{s}\subseteq {t}\right\}\right)\right)$