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

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 ˙ = 0 U
dvh1dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dvh1dim ⊢ φ → ∃ z ∈ 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 ˙ = 0 U
5 dvh1dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
7 1 2 6 5 dvh1dimat ⊢ φ → ∃ p p ∈ LSAtoms ⁡ U
8 1 2 5 dvhlmod ⊢ φ → U ∈ LMod
9 8 adantr ⊢ φ ∧ p ∈ LSAtoms ⁡ U → U ∈ LMod
10 simpr ⊢ φ ∧ p ∈ LSAtoms ⁡ U → p ∈ LSAtoms ⁡ U
11 4 6 9 10 lsateln0 ⊢ φ ∧ p ∈ LSAtoms ⁡ U → ∃ z ∈ p z ≠ 0 ˙
12 3 6 9 10 lsatssv ⊢ φ ∧ p ∈ LSAtoms ⁡ U → p ⊆ V
13 12 sseld ⊢ φ ∧ p ∈ LSAtoms ⁡ U → z ∈ p → z ∈ V
14 13 anim1d ⊢ φ ∧ p ∈ LSAtoms ⁡ U → z ∈ p ∧ z ≠ 0 ˙ → z ∈ V ∧ z ≠ 0 ˙
15 14 reximdv2 ⊢ φ ∧ p ∈ LSAtoms ⁡ U → ∃ z ∈ p z ≠ 0 ˙ → ∃ z ∈ V z ≠ 0 ˙
16 11 15 mpd ⊢ φ ∧ p ∈ LSAtoms ⁡ U → ∃ z ∈ V z ≠ 0 ˙
17 7 16 exlimddv ⊢ φ → ∃ z ∈ V z ≠ 0 ˙