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 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 } ) )