Metamath Proof Explorer

Theorem lspsslco

Description: Lemma for lspeqlco . (Contributed by AV, 17-Apr-2019)

Ref Expression
Hypothesis lspeqvlco.b ⊢ B = Base M
Assertion lspsslco ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → LSpan ⁡ M ⁡ V ⊆ M LinCo V

Proof

Step Hyp Ref Expression
1 lspeqvlco.b ⊢ B = Base M
2 simpl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M ∈ LMod
3 1 pweqi ⊢ 𝒫 B = 𝒫 Base M
4 3 eleq2i ⊢ V ∈ 𝒫 B ↔ V ∈ 𝒫 Base M
5 lincolss ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → M LinCo V ∈ LSubSp ⁡ M
6 4 5 sylan2b ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M LinCo V ∈ LSubSp ⁡ M
7 lcoss ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → V ⊆ M LinCo V
8 4 7 sylan2b ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → V ⊆ M LinCo V
9 eqid ⊢ LSubSp ⁡ M = LSubSp ⁡ M
10 eqid ⊢ LSpan ⁡ M = LSpan ⁡ M
11 9 10 lspssp ⊢ M ∈ LMod ∧ M LinCo V ∈ LSubSp ⁡ M ∧ V ⊆ M LinCo V → LSpan ⁡ M ⁡ V ⊆ M LinCo V
12 2 6 8 11 syl3anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → LSpan ⁡ M ⁡ V ⊆ M LinCo V