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

Metamath Proof Explorer

Theorem lspfval

Description: The span function for a left vector space (or a left module). ( df-span analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspfval ( 𝑊 ∈ 𝑋 → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
6 5 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
7 6 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
9 8 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
10 9 rabeqdv ⊢ ( 𝑤 = 𝑊 → { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } = { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } )
11 10 inteqd ⊢ ( 𝑤 = 𝑊 → ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } = ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } )
12 7 11 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
13 df-lsp ⊢ LSpan = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )
14 1 fvexi ⊢ 𝑉 ∈ V
15 14 pwex ⊢ 𝒫 𝑉 ∈ V
16 15 mptex ⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) ∈ V
17 12 13 16 fvmpt ⊢ ( 𝑊 ∈ V → ( LSpan ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
18 4 17 syl ⊢ ( 𝑊 ∈ 𝑋 → ( LSpan ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
19 3 18 eqtrid ⊢ ( 𝑊 ∈ 𝑋 → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )