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 ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ LSubSp ⁡ w | s ⊆ t

Detailed syntax breakdown

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 ⊆ t
14 13 8 10 crab class t ∈ LSubSp ⁡ w | s ⊆ t
15 14 cint class ⋂ t ∈ LSubSp ⁡ w | s ⊆ t
16 3 7 15 cmpt class s ∈ 𝒫 Base w ⟼ ⋂ t ∈ LSubSp ⁡ w | s ⊆ t
17 1 2 16 cmpt class w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ LSubSp ⁡ w | s ⊆ t
18 0 17 wceq wff LSpan = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ LSubSp ⁡ w | s ⊆ t