Metamath Proof Explorer

Theorem lspval

Description: The span of a set of vectors (in a left module). ( spanval analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspval.v ⊢ V = Base W
lspval.s ⊢ S = LSubSp ⁡ W
lspval.n ⊢ N = LSpan ⁡ W
Assertion lspval ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U = ⋂ t ∈ S | U ⊆ t

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ V = Base W
2 lspval.s ⊢ S = LSubSp ⁡ W
3 lspval.n ⊢ N = LSpan ⁡ W
4 1 2 3 lspfval ⊢ W ∈ LMod → N = s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t
5 4 fveq1d ⊢ W ∈ LMod → N ⁡ U = s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t ⁡ U
6 5 adantr ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U = s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t ⁡ U
7 eqid ⊢ s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t = s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t
8 sseq1 ⊢ s = U → s ⊆ t ↔ U ⊆ t
9 8 rabbidv ⊢ s = U → t ∈ S | s ⊆ t = t ∈ S | U ⊆ t
10 9 inteqd ⊢ s = U → ⋂ t ∈ S | s ⊆ t = ⋂ t ∈ S | U ⊆ t
11 simpr ⊢ W ∈ LMod ∧ U ⊆ V → U ⊆ V
12 1 fvexi ⊢ V ∈ V
13 12 elpw2 ⊢ U ∈ 𝒫 V ↔ U ⊆ V
14 11 13 sylibr ⊢ W ∈ LMod ∧ U ⊆ V → U ∈ 𝒫 V
15 1 2 lss1 ⊢ W ∈ LMod → V ∈ S
16 sseq2 ⊢ t = V → U ⊆ t ↔ U ⊆ V
17 16 rspcev ⊢ V ∈ S ∧ U ⊆ V → ∃ t ∈ S U ⊆ t
18 15 17 sylan ⊢ W ∈ LMod ∧ U ⊆ V → ∃ t ∈ S U ⊆ t
19 intexrab ⊢ ∃ t ∈ S U ⊆ t ↔ ⋂ t ∈ S | U ⊆ t ∈ V
20 18 19 sylib ⊢ W ∈ LMod ∧ U ⊆ V → ⋂ t ∈ S | U ⊆ t ∈ V
21 7 10 14 20 fvmptd3 ⊢ W ∈ LMod ∧ U ⊆ V → s ∈ 𝒫 V ⟼ ⋂ t ∈ S | s ⊆ t ⁡ U = ⋂ t ∈ S | U ⊆ t
22 6 21 eqtrd ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U = ⋂ t ∈ S | U ⊆ t