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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dvh1dim.o ⊢ 0 = ( 0g ‘ 𝑈 )
dvh1dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion dvh1dim ( 𝜑 → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ 0 )

Proof

Step Hyp Ref Expression
1 dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dvh1dim.o ⊢ 0 = ( 0g ‘ 𝑈 )
5 dvh1dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
7 1 2 6 5 dvh1dimat ⊢ ( 𝜑 → ∃ 𝑝 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) )
8 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) )
11 4 6 9 10 lsateln0 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑝 𝑧 ≠ 0 )
12 3 6 9 10 lsatssv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑝 ⊆ 𝑉 )
13 12 sseld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( 𝑧 ∈ 𝑝 → 𝑧 ∈ 𝑉 ) )
14 13 anim1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ( 𝑧 ∈ 𝑝 ∧ 𝑧 ≠ 0 ) → ( 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 0 ) ) )
15 14 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑝 𝑧 ≠ 0 → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ 0 ) )
16 11 15 mpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ 0 )
17 7 16 exlimddv ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ 0 )