Metamath Proof Explorer

Theorem lsatspn0

Description: The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses lsatspn0.v 
|- V = ( Base ` W )
lsatspn0.n 
|- N = ( LSpan ` W )
lsatspn0.o 
|- .0. = ( 0g ` W )
lsatspn0.a 
|- A = ( LSAtoms ` W )
isateln0.w 
|- ( ph -> W e. LMod )
isateln0.x 
|- ( ph -> X e. V )
Assertion lsatspn0 
|- ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) )

Proof

Step Hyp Ref Expression
1 lsatspn0.v 
 |-  V = ( Base ` W )
2 lsatspn0.n 
 |-  N = ( LSpan ` W )
3 lsatspn0.o 
 |-  .0. = ( 0g ` W )
4 lsatspn0.a 
 |-  A = ( LSAtoms ` W )
5 isateln0.w 
 |-  ( ph -> W e. LMod )
6 isateln0.x 
 |-  ( ph -> X e. V )
7 5 adantr 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> W e. LMod )
8 simpr 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> ( N ` { X } ) e. A )
9 3 4 7 8 lsatn0 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> ( N ` { X } ) =/= { .0. } )
10 sneq 
 |-  ( X = .0. -> { X } = { .0. } )
11 10 fveq2d 
 |-  ( X = .0. -> ( N ` { X } ) = ( N ` { .0. } ) )
12 11 adantl 
 |-  ( ( ( ph /\ ( N ` { X } ) e. A ) /\ X = .0. ) -> ( N ` { X } ) = ( N ` { .0. } ) )
13 7 adantr 
 |-  ( ( ( ph /\ ( N ` { X } ) e. A ) /\ X = .0. ) -> W e. LMod )
14 3 2 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
15 13 14 syl 
 |-  ( ( ( ph /\ ( N ` { X } ) e. A ) /\ X = .0. ) -> ( N ` { .0. } ) = { .0. } )
16 12 15 eqtrd 
 |-  ( ( ( ph /\ ( N ` { X } ) e. A ) /\ X = .0. ) -> ( N ` { X } ) = { .0. } )
17 16 ex 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> ( X = .0. -> ( N ` { X } ) = { .0. } ) )
18 17 necon3d 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> ( ( N ` { X } ) =/= { .0. } -> X =/= .0. ) )
19 9 18 mpd 
 |-  ( ( ph /\ ( N ` { X } ) e. A ) -> X =/= .0. )
20 5 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> W e. LMod )
21 6 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> X e. V )
22 simpr 
 |-  ( ( ph /\ X =/= .0. ) -> X =/= .0. )
23 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
24 21 22 23 sylanbrc 
 |-  ( ( ph /\ X =/= .0. ) -> X e. ( V \ { .0. } ) )
25 1 2 3 4 20 24 lsatlspsn 
 |-  ( ( ph /\ X =/= .0. ) -> ( N ` { X } ) e. A )
26 19 25 impbida 
 |-  ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) )