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 )