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