Definition df-lsp 20149

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 = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

Distinct variable group:   𝑤,𝑠,𝑡

Detailed syntax breakdown of Definition df-lsp

Step	Hyp	Ref	Expression
1		clspn 20148	. 2 class LSpan
2		vw	. . 3 setvar 𝑤
3		cvv 3422	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1538	. . . . . 6 class 𝑤
6		cbs 16840	. . . . . 6 class Base
7	5, 6	cfv 6418	. . . . 5 class (Base‘𝑤)
8	7	cpw 4530	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1538	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1538	. . . . . . 7 class 𝑡
12	9, 11	wss 3883	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		clss 20108	. . . . . . 7 class LSubSp
14	5, 13	cfv 6418	. . . . . 6 class (LSubSp‘𝑤)
15	12, 10, 14	crab 3067	. . . . 5 class {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}
16	15	cint 4876	. . . 4 class ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}
17	4, 8, 16	cmpt 5153	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡})
18	2, 3, 17	cmpt 5153	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
19	1, 18	wceq 1539	1 wff LSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

This definition is referenced by:  lspfval  20150