Metamath Proof Explorer

Theorem lspsnid

Description: A vector belongs to the span of its singleton. ( spansnid analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypotheses	lspsnid.v	$⊢ V = {Base}_{W}$
		lspsnid.n	$⊢ N = LSpan (W)$
	Assertion	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		lspsnid.v	$⊢ V = {Base}_{W}$
2		lspsnid.n	$⊢ N = LSpan (W)$
3		snssi	$⊢ X \in V \to \{X\} \subseteq V$
4	1 2	lspssid	$⊢ (W \in LMod \land \{X\} \subseteq V) \to \{X\} \subseteq N (\{X\})$
5	3 4	sylan2	$⊢ (W \in LMod \land X \in V) \to \{X\} \subseteq N (\{X\})$
6		snssg	$⊢ X \in V \to (X \in N (\{X\}) \leftrightarrow \{X\} \subseteq N (\{X\}))$
7	6	adantl	$⊢ (W \in LMod \land X \in V) \to (X \in N (\{X\}) \leftrightarrow \{X\} \subseteq N (\{X\}))$
8	5 7	mpbird	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$