This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑤 ∈ 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 ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )