dvh2dim

Description: There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dvh3dim.h	$⊢ H = LHyp (K)$
	dvh3dim.u	$⊢ U = DVecH (K) (W)$
	dvh3dim.v	$⊢ V = {Base}_{U}$
	dvh3dim.n	$⊢ N = LSpan (U)$
	dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
	dvh3dim.x	$⊢ φ \to X \in V$
Assertion	dvh2dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X\})$

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		dvh3dim.n	$⊢ N = LSpan (U)$
5		dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dvh3dim.x	$⊢ φ \to X \in V$
7		eqid	$⊢ 0_{U} = 0_{U}$
8	1 2 3 7 5	dvh1dim	$⊢ φ \to \exists z \in V z \neq 0_{U}$
9	8	adantr	$⊢ (φ \land X = 0_{U}) \to \exists z \in V z \neq 0_{U}$
10		simpr	$⊢ (φ \land X = 0_{U}) \to X = 0_{U}$
11	10	sneqd	$⊢ (φ \land X = 0_{U}) \to \{X\} = \{0_{U}\}$
12	11	fveq2d	$⊢ (φ \land X = 0_{U}) \to N (\{X\}) = N (\{0_{U}\})$
13	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
14	7 4	lspsn0	$⊢ U \in LMod \to N (\{0_{U}\}) = \{0_{U}\}$
15	13 14	syl	$⊢ φ \to N (\{0_{U}\}) = \{0_{U}\}$
16	15	adantr	$⊢ (φ \land X = 0_{U}) \to N (\{0_{U}\}) = \{0_{U}\}$
17	12 16	eqtrd	$⊢ (φ \land X = 0_{U}) \to N (\{X\}) = \{0_{U}\}$
18	17	eleq2d	$⊢ (φ \land X = 0_{U}) \to (z \in N (\{X\}) \leftrightarrow z \in \{0_{U}\})$
19		velsn	$⊢ z \in \{0_{U}\} \leftrightarrow z = 0_{U}$
20	18 19	bitrdi	$⊢ (φ \land X = 0_{U}) \to (z \in N (\{X\}) \leftrightarrow z = 0_{U})$
21	20	necon3bbid	$⊢ (φ \land X = 0_{U}) \to (\neg z \in N (\{X\}) \leftrightarrow z \neq 0_{U})$
22	21	rexbidv	$⊢ (φ \land X = 0_{U}) \to (\exists z \in V \neg z \in N (\{X\}) \leftrightarrow \exists z \in V z \neq 0_{U})$
23	9 22	mpbird	$⊢ (φ \land X = 0_{U}) \to \exists z \in V \neg z \in N (\{X\})$
24	5	adantr	$⊢ (φ \land X \neq 0_{U}) \to (K \in HL \land W \in H)$
25	6	adantr	$⊢ (φ \land X \neq 0_{U}) \to X \in V$
26		simpr	$⊢ (φ \land X \neq 0_{U}) \to X \neq 0_{U}$
27	1 2 3 4 24 25 25 7 26 26	dvhdimlem	$⊢ (φ \land X \neq 0_{U}) \to \exists z \in V \neg z \in N (\{X, X\})$
28		dfsn2	$⊢ \{X\} = \{X, X\}$
29	28	fveq2i	$⊢ N (\{X\}) = N (\{X, X\})$
30	29	eleq2i	$⊢ z \in N (\{X\}) \leftrightarrow z \in N (\{X, X\})$
31	30	notbii	$⊢ \neg z \in N (\{X\}) \leftrightarrow \neg z \in N (\{X, X\})$
32	31	rexbii	$⊢ \exists z \in V \neg z \in N (\{X\}) \leftrightarrow \exists z \in V \neg z \in N (\{X, X\})$
33	27 32	sylibr	$⊢ (φ \land X \neq 0_{U}) \to \exists z \in V \neg z \in N (\{X\})$
34	23 33	pm2.61dane	$⊢ φ \to \exists z \in V \neg z \in N (\{X\})$

Metamath Proof Explorer

Theorem dvh2dim

Proof