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

Metamath Proof Explorer

Theorem lspsneq0

Description: Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspsneq0.v 
|- V = ( Base ` W )
lspsneq0.z 
|- .0. = ( 0g ` W )
lspsneq0.n 
|- N = ( LSpan ` W )
Assertion lspsneq0 
|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 lspsneq0.v 
 |-  V = ( Base ` W )
2 lspsneq0.z 
 |-  .0. = ( 0g ` W )
3 lspsneq0.n 
 |-  N = ( LSpan ` W )
4 1 3 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
5 eleq2 
 |-  ( ( N ` { X } ) = { .0. } -> ( X e. ( N ` { X } ) <-> X e. { .0. } ) )
6 4 5 syl5ibcom 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } -> X e. { .0. } ) )
7 elsni 
 |-  ( X e. { .0. } -> X = .0. )
8 6 7 syl6 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } -> X = .0. ) )
9 2 3 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
10 9 adantr 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { .0. } ) = { .0. } )
11 sneq 
 |-  ( X = .0. -> { X } = { .0. } )
12 11 fveqeq2d 
 |-  ( X = .0. -> ( ( N ` { X } ) = { .0. } <-> ( N ` { .0. } ) = { .0. } ) )
13 10 12 syl5ibrcom 
 |-  ( ( W e. LMod /\ X e. V ) -> ( X = .0. -> ( N ` { X } ) = { .0. } ) )
14 8 13 impbid 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )