Metamath Proof Explorer

Theorem lspsnss

Description: The span of the singleton of a subspace member is included in the subspace. ( spansnss analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 4-Sep-2014)

	Ref	Expression
Hypotheses	lspsnss.s	$⊢ S = LSubSp (W)$
	lspsnss.n	$⊢ N = LSpan (W)$
Assertion	lspsnss	$⊢ (W \in LMod \land U \in S \land X \in U) \to N (\{X\}) \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	$⊢ S = LSubSp (W)$
2		lspsnss.n	$⊢ N = LSpan (W)$
3		snssi	$⊢ X \in U \to \{X\} \subseteq U$
4	1 2	lspssp	$⊢ (W \in LMod \land U \in S \land \{X\} \subseteq U) \to N (\{X\}) \subseteq U$
5	3 4	syl3an3	$⊢ (W \in LMod \land U \in S \land X \in U) \to N (\{X\}) \subseteq U$