dvh3dim

Description: There is a vector that is outside the span of 2 others. (Contributed by NM, 24-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$
	dvh3dim.y	$⊢ φ \to Y \in V$
Assertion	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y\})$

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		dvh3dim.y	$⊢ φ \to Y \in V$
8	1 2 3 4 5 7	dvh2dim	$⊢ φ \to \exists z \in V \neg z \in N (\{Y\})$
9	8	adantr	$⊢ (φ \land X = 0_{U}) \to \exists z \in V \neg z \in N (\{Y\})$
10		prcom	$⊢ \{X, Y\} = \{Y, X\}$
11		preq2	$⊢ X = 0_{U} \to \{Y, X\} = \{Y, 0_{U}\}$
12	10 11	syl5eq	$⊢ X = 0_{U} \to \{X, Y\} = \{Y, 0_{U}\}$
13	12	fveq2d	$⊢ X = 0_{U} \to N (\{X, Y\}) = N (\{Y, 0_{U}\})$
14		eqid	$⊢ 0_{U} = 0_{U}$
15	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
16	3 14 4 15 7	lsppr0	$⊢ φ \to N (\{Y, 0_{U}\}) = N (\{Y\})$
17	13 16	sylan9eqr	$⊢ (φ \land X = 0_{U}) \to N (\{X, Y\}) = N (\{Y\})$
18	17	eleq2d	$⊢ (φ \land X = 0_{U}) \to (z \in N (\{X, Y\}) \leftrightarrow z \in N (\{Y\}))$
19	18	notbid	$⊢ (φ \land X = 0_{U}) \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg z \in N (\{Y\}))$
20	19	rexbidv	$⊢ (φ \land X = 0_{U}) \to (\exists z \in V \neg z \in N (\{X, Y\}) \leftrightarrow \exists z \in V \neg z \in N (\{Y\}))$
21	9 20	mpbird	$⊢ (φ \land X = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y\})$
22	1 2 3 4 5 6	dvh2dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X\})$
23	22	adantr	$⊢ (φ \land Y = 0_{U}) \to \exists z \in V \neg z \in N (\{X\})$
24		preq2	$⊢ Y = 0_{U} \to \{X, Y\} = \{X, 0_{U}\}$
25	24	fveq2d	$⊢ Y = 0_{U} \to N (\{X, Y\}) = N (\{X, 0_{U}\})$
26	3 14 4 15 6	lsppr0	$⊢ φ \to N (\{X, 0_{U}\}) = N (\{X\})$
27	25 26	sylan9eqr	$⊢ (φ \land Y = 0_{U}) \to N (\{X, Y\}) = N (\{X\})$
28	27	eleq2d	$⊢ (φ \land Y = 0_{U}) \to (z \in N (\{X, Y\}) \leftrightarrow z \in N (\{X\}))$
29	28	notbid	$⊢ (φ \land Y = 0_{U}) \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg z \in N (\{X\}))$
30	29	rexbidv	$⊢ (φ \land Y = 0_{U}) \to (\exists z \in V \neg z \in N (\{X, Y\}) \leftrightarrow \exists z \in V \neg z \in N (\{X\}))$
31	23 30	mpbird	$⊢ (φ \land Y = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y\})$
32	5	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to (K \in HL \land W \in H)$
33	6	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \in V$
34	7	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \in V$
35		simprl	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \neq 0_{U}$
36		simprr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \neq 0_{U}$
37	1 2 3 4 32 33 34 14 35 36	dvhdimlem	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to \exists z \in V \neg z \in N (\{X, Y\})$
38	21 31 37	pm2.61da2ne	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y\})$

Metamath Proof Explorer

Theorem dvh3dim

Proof