Metamath Proof Explorer

Theorem lsateln0

Description: A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses lsateln0.z 
|- .0. = ( 0g ` W )
lsateln0.a 
|- A = ( LSAtoms ` W )
lsateln0.w 
|- ( ph -> W e. LMod )
lsateln0.u 
|- ( ph -> U e. A )
Assertion lsateln0 
|- ( ph -> E. v e. U v =/= .0. )

Proof

Step Hyp Ref Expression
1 lsateln0.z 
 |-  .0. = ( 0g ` W )
2 lsateln0.a 
 |-  A = ( LSAtoms ` W )
3 lsateln0.w 
 |-  ( ph -> W e. LMod )
4 lsateln0.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 eldifi 
 |-  ( v e. ( ( Base ` W ) \ { .0. } ) -> v e. ( Base ` W ) )
11 5 6 lspsnid 
 |-  ( ( W e. LMod /\ v e. ( Base ` W ) ) -> v e. ( ( LSpan ` W ) ` { v } ) )
12 3 10 11 syl2an 
 |-  ( ( ph /\ v e. ( ( Base ` W ) \ { .0. } ) ) -> v e. ( ( LSpan ` W ) ` { v } ) )
13 eleq2 
 |-  ( U = ( ( LSpan ` W ) ` { v } ) -> ( v e. U <-> v e. ( ( LSpan ` W ) ` { v } ) ) )
14 12 13 syl5ibrcom 
 |-  ( ( ph /\ v e. ( ( Base ` W ) \ { .0. } ) ) -> ( U = ( ( LSpan ` W ) ` { v } ) -> v e. U ) )
15 14 reximdva 
 |-  ( ph -> ( E. v e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { v } ) -> E. v e. ( ( Base ` W ) \ { .0. } ) v e. U ) )
16 9 15 mpd 
 |-  ( ph -> E. v e. ( ( Base ` W ) \ { .0. } ) v e. U )
17 eldifsn 
 |-  ( v e. ( ( Base ` W ) \ { .0. } ) <-> ( v e. ( Base ` W ) /\ v =/= .0. ) )
18 17 anbi1i 
 |-  ( ( v e. ( ( Base ` W ) \ { .0. } ) /\ v e. U ) <-> ( ( v e. ( Base ` W ) /\ v =/= .0. ) /\ v e. U ) )
19 anass 
 |-  ( ( ( v e. ( Base ` W ) /\ v =/= .0. ) /\ v e. U ) <-> ( v e. ( Base ` W ) /\ ( v =/= .0. /\ v e. U ) ) )
20 18 19 bitri 
 |-  ( ( v e. ( ( Base ` W ) \ { .0. } ) /\ v e. U ) <-> ( v e. ( Base ` W ) /\ ( v =/= .0. /\ v e. U ) ) )
21 20 simprbi 
 |-  ( ( v e. ( ( Base ` W ) \ { .0. } ) /\ v e. U ) -> ( v =/= .0. /\ v e. U ) )
22 21 ancomd 
 |-  ( ( v e. ( ( Base ` W ) \ { .0. } ) /\ v e. U ) -> ( v e. U /\ v =/= .0. ) )
23 22 reximi2 
 |-  ( E. v e. ( ( Base ` W ) \ { .0. } ) v e. U -> E. v e. U v =/= .0. )
24 16 23 syl 
 |-  ( ph -> E. v e. U v =/= .0. )