Metamath Proof Explorer

Theorem dvh1dim

Description: There exists a nonzero vector. (Contributed by NM, 26-Apr-2015)

Ref Expression
Hypotheses dvh3dim.h 
|- H = ( LHyp ` K )
dvh3dim.u 
|- U = ( ( DVecH ` K ) ` W )
dvh3dim.v 
|- V = ( Base ` U )
dvh1dim.o 
|- .0. = ( 0g ` U )
dvh1dim.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dvh1dim 
|- ( ph -> E. z e. V z =/= .0. )

Proof

Step Hyp Ref Expression
1 dvh3dim.h 
 |-  H = ( LHyp ` K )
2 dvh3dim.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dvh3dim.v 
 |-  V = ( Base ` U )
4 dvh1dim.o 
 |-  .0. = ( 0g ` U )
5 dvh1dim.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
7 1 2 6 5 dvh1dimat 
 |-  ( ph -> E. p p e. ( LSAtoms ` U ) )
8 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
9 8 adantr 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> U e. LMod )
10 simpr 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> p e. ( LSAtoms ` U ) )
11 4 6 9 10 lsateln0 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> E. z e. p z =/= .0. )
12 3 6 9 10 lsatssv 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> p C_ V )
13 12 sseld 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> ( z e. p -> z e. V ) )
14 13 anim1d 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> ( ( z e. p /\ z =/= .0. ) -> ( z e. V /\ z =/= .0. ) ) )
15 14 reximdv2 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> ( E. z e. p z =/= .0. -> E. z e. V z =/= .0. ) )
16 11 15 mpd 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) ) -> E. z e. V z =/= .0. )
17 7 16 exlimddv 
 |-  ( ph -> E. z e. V z =/= .0. )