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	$⊢ \underset{˙}{0} = 0_{U}$
	dvh1dim.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	dvh1dim	$⊢ φ \to \exists z \in V z \neq \underset{˙}{0}$

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	$⊢ \underset{˙}{0} = 0_{U}$
5		dvh1dim.k	$⊢ φ \to (K \in HL \land W \in H)$
6		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
7	1 2 6 5	dvh1dimat	$⊢ φ \to \exists p p \in LSAtoms (U)$
8	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
9	8	adantr	$⊢ (φ \land p \in LSAtoms (U)) \to U \in LMod$
10		simpr	$⊢ (φ \land p \in LSAtoms (U)) \to p \in LSAtoms (U)$
11	4 6 9 10	lsateln0	$⊢ (φ \land p \in LSAtoms (U)) \to \exists z \in p z \neq \underset{˙}{0}$
12	3 6 9 10	lsatssv	$⊢ (φ \land p \in LSAtoms (U)) \to p \subseteq V$
13	12	sseld	$⊢ (φ \land p \in LSAtoms (U)) \to (z \in p \to z \in V)$
14	13	anim1d	$⊢ (φ \land p \in LSAtoms (U)) \to ((z \in p \land z \neq \underset{˙}{0}) \to (z \in V \land z \neq \underset{˙}{0}))$
15	14	reximdv2	$⊢ (φ \land p \in LSAtoms (U)) \to (\exists z \in p z \neq \underset{˙}{0} \to \exists z \in V z \neq \underset{˙}{0})$
16	11 15	mpd	$⊢ (φ \land p \in LSAtoms (U)) \to \exists z \in V z \neq \underset{˙}{0}$
17	7 16	exlimddv	$⊢ φ \to \exists z \in V z \neq \underset{˙}{0}$

Metamath Proof Explorer