lspsslco

		Ref	Expression
	Hypothesis	lspeqvlco.b	$⊢ B = {Base}_{M}$
	Assertion	lspsslco	$⊢ (M \in LMod \land V \in 𝒫 B) \to LSpan (M) (V) \subseteq M LinCo V$

Step	Hyp	Ref	Expression
1		lspeqvlco.b	$⊢ B = {Base}_{M}$
2		simpl	$⊢ (M \in LMod \land V \in 𝒫 B) \to M \in LMod$
3	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
4	3	eleq2i	$⊢ V \in 𝒫 B \leftrightarrow V \in 𝒫 {Base}_{M}$
5		lincolss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo V \in LSubSp (M)$
6	4 5	sylan2b	$⊢ (M \in LMod \land V \in 𝒫 B) \to M LinCo V \in LSubSp (M)$
7		lcoss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \subseteq M LinCo V$
8	4 7	sylan2b	$⊢ (M \in LMod \land V \in 𝒫 B) \to V \subseteq M LinCo V$
9		eqid	$⊢ LSubSp (M) = LSubSp (M)$
10		eqid	$⊢ LSpan (M) = LSpan (M)$
11	9 10	lspssp	$⊢ (M \in LMod \land M LinCo V \in LSubSp (M) \land V \subseteq M LinCo V) \to LSpan (M) (V) \subseteq M LinCo V$
12	2 6 8 11	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B) \to LSpan (M) (V) \subseteq M LinCo V$

Metamath Proof Explorer