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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clspn	⊢ LSpan
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		vt	⊢ 𝑡
9		clss	⊢ LSubSp
10	5 9	cfv	⊢ ( LSubSp ‘ 𝑤 )
11	3	cv	⊢ 𝑠
12	8	cv	⊢ 𝑡
13	11 12	wss	⊢ 𝑠 ⊆ 𝑡
14	13 8 10	crab	⊢ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 }
15	14	cint	⊢ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 }
16	3 7 15	cmpt	⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } )
17	1 2 16	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )
18	0 17	wceq	⊢ LSpan = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )