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 \in V ⟼ (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in LSubSp (w) \| s \subseteq t\}))$

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

Metamath Proof Explorer