lcosslsp

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

Proof

Step	Hyp	Ref	Expression
1		lspeqvlco.b	$⊢ B = {Base}_{M}$
2		ellcoellss	$⊢ (M \in LMod \land s \in LSubSp (M) \land V \subseteq s) \to \forall y \in (M LinCo V) y \in s$
3	2	3exp	$⊢ M \in LMod \to (s \in LSubSp (M) \to (V \subseteq s \to \forall y \in (M LinCo V) y \in s))$
4	3	ad2antrr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to (s \in LSubSp (M) \to (V \subseteq s \to \forall y \in (M LinCo V) y \in s))$
5	4	imp	$⊢ (((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \land s \in LSubSp (M)) \to (V \subseteq s \to \forall y \in (M LinCo V) y \in s)$
6		elequ1	$⊢ y = x \to (y \in s \leftrightarrow x \in s)$
7	6	rspcv	$⊢ x \in (M LinCo V) \to (\forall y \in (M LinCo V) y \in s \to x \in s)$
8	7	ad2antlr	$⊢ (((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \land s \in LSubSp (M)) \to (\forall y \in (M LinCo V) y \in s \to x \in s)$
9	5 8	syld	$⊢ (((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \land s \in LSubSp (M)) \to (V \subseteq s \to x \in s)$
10	9	ralrimiva	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to \forall s \in LSubSp (M) (V \subseteq s \to x \in s)$
11		vex	$⊢ x \in V$
12	11	elintrab	$⊢ x \in ⋂ \{s \in LSubSp (M) \| V \subseteq s\} \leftrightarrow \forall s \in LSubSp (M) (V \subseteq s \to x \in s)$
13	10 12	sylibr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to x \in ⋂ \{s \in LSubSp (M) \| V \subseteq s\}$
14		simpll	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to M \in LMod$
15		elpwi	$⊢ V \in 𝒫 B \to V \subseteq B$
16	15	ad2antlr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to V \subseteq B$
17		eqid	$⊢ LSubSp (M) = LSubSp (M)$
18		eqid	$⊢ LSpan (M) = LSpan (M)$
19	1 17 18	lspval	$⊢ (M \in LMod \land V \subseteq B) \to LSpan (M) (V) = ⋂ \{s \in LSubSp (M) \| V \subseteq s\}$
20	14 16 19	syl2anc	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to LSpan (M) (V) = ⋂ \{s \in LSubSp (M) \| V \subseteq s\}$
21	13 20	eleqtrrd	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in (M LinCo V)) \to x \in LSpan (M) (V)$
22	21	ex	$⊢ (M \in LMod \land V \in 𝒫 B) \to (x \in (M LinCo V) \to x \in LSpan (M) (V))$
23	22	ssrdv	$⊢ (M \in LMod \land V \in 𝒫 B) \to M LinCo V \subseteq LSpan (M) (V)$

Metamath Proof Explorer

Theorem lcosslsp

Proof