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

Metamath Proof Explorer

Theorem lsatn0

Description: A 1-dim subspace (atom) of a left module or left vector space is nonzero. ( atne0 analog.) (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatn0.o 
|- .0. = ( 0g ` W )
lsatn0.a 
|- A = ( LSAtoms ` W )
lsatn0.w 
|- ( ph -> W e. LMod )
lsatn0.u 
|- ( ph -> U e. A )
Assertion lsatn0 
|- ( ph -> U =/= { .0. } )

Proof

Step Hyp Ref Expression
1 lsatn0.o 
 |-  .0. = ( 0g ` W )
2 lsatn0.a 
 |-  A = ( LSAtoms ` W )
3 lsatn0.w 
 |-  ( ph -> W e. LMod )
4 lsatn0.u 
 |-  ( ph -> U e. A )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
7 5 6 1 2 islsat 
 |-  ( W e. LMod -> ( U e. A <-> E. v e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { v } ) ) )
8 3 7 syl 
 |-  ( ph -> ( U e. A <-> E. v e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { v } ) ) )
9 4 8 mpbid 
 |-  ( ph -> E. v e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { v } ) )
10 eldifsn 
 |-  ( v e. ( ( Base ` W ) \ { .0. } ) <-> ( v e. ( Base ` W ) /\ v =/= .0. ) )
11 5 1 6 lspsneq0 
 |-  ( ( W e. LMod /\ v e. ( Base ` W ) ) -> ( ( ( LSpan ` W ) ` { v } ) = { .0. } <-> v = .0. ) )
12 3 11 sylan 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> ( ( ( LSpan ` W ) ` { v } ) = { .0. } <-> v = .0. ) )
13 12 biimpd 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> ( ( ( LSpan ` W ) ` { v } ) = { .0. } -> v = .0. ) )
14 13 necon3d 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> ( v =/= .0. -> ( ( LSpan ` W ) ` { v } ) =/= { .0. } ) )
15 14 expimpd 
 |-  ( ph -> ( ( v e. ( Base ` W ) /\ v =/= .0. ) -> ( ( LSpan ` W ) ` { v } ) =/= { .0. } ) )
16 10 15 biimtrid 
 |-  ( ph -> ( v e. ( ( Base ` W ) \ { .0. } ) -> ( ( LSpan ` W ) ` { v } ) =/= { .0. } ) )
17 neeq1 
 |-  ( U = ( ( LSpan ` W ) ` { v } ) -> ( U =/= { .0. } <-> ( ( LSpan ` W ) ` { v } ) =/= { .0. } ) )
18 17 biimprcd 
 |-  ( ( ( LSpan ` W ) ` { v } ) =/= { .0. } -> ( U = ( ( LSpan ` W ) ` { v } ) -> U =/= { .0. } ) )
19 16 18 syl6 
 |-  ( ph -> ( v e. ( ( Base ` W ) \ { .0. } ) -> ( U = ( ( LSpan ` W ) ` { v } ) -> U =/= { .0. } ) ) )
20 19 rexlimdv 
 |-  ( ph -> ( E. v e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { v } ) -> U =/= { .0. } ) )
21 9 20 mpd 
 |-  ( ph -> U =/= { .0. } )