This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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