# Metamath Proof Explorer

## Theorem dvh1dim

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

Ref Expression
Hypotheses dvh3dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dvh1dim.o
dvh1dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion dvh1dim

### Proof

Step Hyp Ref Expression
1 dvh3dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dvh1dim.o
5 dvh1dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
7 1 2 6 5 dvh1dimat ${⊢}{\phi }\to \exists {p}\phantom{\rule{.4em}{0ex}}{p}\in \mathrm{LSAtoms}\left({U}\right)$
8 1 2 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
9 8 adantr ${⊢}\left({\phi }\wedge {p}\in \mathrm{LSAtoms}\left({U}\right)\right)\to {U}\in \mathrm{LMod}$
10 simpr ${⊢}\left({\phi }\wedge {p}\in \mathrm{LSAtoms}\left({U}\right)\right)\to {p}\in \mathrm{LSAtoms}\left({U}\right)$
11 4 6 9 10 lsateln0
12 3 6 9 10 lsatssv ${⊢}\left({\phi }\wedge {p}\in \mathrm{LSAtoms}\left({U}\right)\right)\to {p}\subseteq {V}$
13 12 sseld ${⊢}\left({\phi }\wedge {p}\in \mathrm{LSAtoms}\left({U}\right)\right)\to \left({z}\in {p}\to {z}\in {V}\right)$
14 13 anim1d
15 14 reximdv2
16 11 15 mpd
17 7 16 exlimddv