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 e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnid.v	|- V = ( Base ` W )
2		lspsnid.n	|- N = ( LSpan ` W )
3		snssi	|- ( X e. V -> { X } C_ V )
4	1 2	lspssid	|- ( ( W e. LMod /\ { X } C_ V ) -> { X } C_ ( N ` { X } ) )
5	3 4	sylan2	|- ( ( W e. LMod /\ X e. V ) -> { X } C_ ( N ` { X } ) )
6		snssg	|- ( X e. V -> ( X e. ( N ` { X } ) <-> { X } C_ ( N ` { X } ) ) )
7	6	adantl	|- ( ( W e. LMod /\ X e. V ) -> ( X e. ( N ` { X } ) <-> { X } C_ ( N ` { X } ) ) )
8	5 7	mpbird	|- ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )