dvh4dimN

Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015) (New usage is discouraged.)

	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$
	dvh3dim2.z	$⊢ φ \to Z \in V$
Assertion	dvh4dimN	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y, Z\})$

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		dvh3dim2.z	$⊢ φ \to Z \in V$
9	1 2 3 4 5 7 8	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{Y, Z\})$
10	9	adantr	$⊢ (φ \land X = 0_{U}) \to \exists z \in V \neg z \in N (\{Y, Z\})$
11		eqid	$⊢ 0_{U} = 0_{U}$
12	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
13		prssi	$⊢ (Y \in V \land Z \in V) \to \{Y, Z\} \subseteq V$
14	7 8 13	syl2anc	$⊢ φ \to \{Y, Z\} \subseteq V$
15	3 11 4 12 14	lspun0	$⊢ φ \to N (\{Y, Z\} \cup \{0_{U}\}) = N (\{Y, Z\})$
16		tpeq1	$⊢ X = 0_{U} \to \{X, Y, Z\} = \{0_{U}, Y, Z\}$
17		tprot	$⊢ \{0_{U}, Y, Z\} = \{Y, Z, 0_{U}\}$
18		df-tp	$⊢ \{Y, Z, 0_{U}\} = \{Y, Z\} \cup \{0_{U}\}$
19	17 18	eqtr2i	$⊢ \{Y, Z\} \cup \{0_{U}\} = \{0_{U}, Y, Z\}$
20	16 19	syl6reqr	$⊢ X = 0_{U} \to \{Y, Z\} \cup \{0_{U}\} = \{X, Y, Z\}$
21	20	fveq2d	$⊢ X = 0_{U} \to N (\{Y, Z\} \cup \{0_{U}\}) = N (\{X, Y, Z\})$
22	15 21	sylan9req	$⊢ (φ \land X = 0_{U}) \to N (\{Y, Z\}) = N (\{X, Y, Z\})$
23	22	eleq2d	$⊢ (φ \land X = 0_{U}) \to (z \in N (\{Y, Z\}) \leftrightarrow z \in N (\{X, Y, Z\}))$
24	23	notbid	$⊢ (φ \land X = 0_{U}) \to (\neg z \in N (\{Y, Z\}) \leftrightarrow \neg z \in N (\{X, Y, Z\}))$
25	24	rexbidv	$⊢ (φ \land X = 0_{U}) \to (\exists z \in V \neg z \in N (\{Y, Z\}) \leftrightarrow \exists z \in V \neg z \in N (\{X, Y, Z\}))$
26	10 25	mpbid	$⊢ (φ \land X = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y, Z\})$
27	1 2 3 4 5 6 8	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Z\})$
28	27	adantr	$⊢ (φ \land Y = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Z\})$
29		prssi	$⊢ (X \in V \land Z \in V) \to \{X, Z\} \subseteq V$
30	6 8 29	syl2anc	$⊢ φ \to \{X, Z\} \subseteq V$
31	3 11 4 12 30	lspun0	$⊢ φ \to N (\{X, Z\} \cup \{0_{U}\}) = N (\{X, Z\})$
32		tpeq2	$⊢ Y = 0_{U} \to \{X, Y, Z\} = \{X, 0_{U}, Z\}$
33		df-tp	$⊢ \{X, Z, 0_{U}\} = \{X, Z\} \cup \{0_{U}\}$
34		tpcomb	$⊢ \{X, Z, 0_{U}\} = \{X, 0_{U}, Z\}$
35	33 34	eqtr3i	$⊢ \{X, Z\} \cup \{0_{U}\} = \{X, 0_{U}, Z\}$
36	32 35	syl6reqr	$⊢ Y = 0_{U} \to \{X, Z\} \cup \{0_{U}\} = \{X, Y, Z\}$
37	36	fveq2d	$⊢ Y = 0_{U} \to N (\{X, Z\} \cup \{0_{U}\}) = N (\{X, Y, Z\})$
38	31 37	sylan9req	$⊢ (φ \land Y = 0_{U}) \to N (\{X, Z\}) = N (\{X, Y, Z\})$
39	38	eleq2d	$⊢ (φ \land Y = 0_{U}) \to (z \in N (\{X, Z\}) \leftrightarrow z \in N (\{X, Y, Z\}))$
40	39	notbid	$⊢ (φ \land Y = 0_{U}) \to (\neg z \in N (\{X, Z\}) \leftrightarrow \neg z \in N (\{X, Y, Z\}))$
41	40	rexbidv	$⊢ (φ \land Y = 0_{U}) \to (\exists z \in V \neg z \in N (\{X, Z\}) \leftrightarrow \exists z \in V \neg z \in N (\{X, Y, Z\}))$
42	28 41	mpbid	$⊢ (φ \land Y = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y, Z\})$
43	1 2 3 4 5 6 7	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y\})$
44	43	adantr	$⊢ (φ \land Z = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y\})$
45		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
46	6 7 45	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
47	3 11 4 12 46	lspun0	$⊢ φ \to N (\{X, Y\} \cup \{0_{U}\}) = N (\{X, Y\})$
48		tpeq3	$⊢ Z = 0_{U} \to \{X, Y, Z\} = \{X, Y, 0_{U}\}$
49		df-tp	$⊢ \{X, Y, 0_{U}\} = \{X, Y\} \cup \{0_{U}\}$
50	48 49	syl6req	$⊢ Z = 0_{U} \to \{X, Y\} \cup \{0_{U}\} = \{X, Y, Z\}$
51	50	fveq2d	$⊢ Z = 0_{U} \to N (\{X, Y\} \cup \{0_{U}\}) = N (\{X, Y, Z\})$
52	47 51	sylan9req	$⊢ (φ \land Z = 0_{U}) \to N (\{X, Y\}) = N (\{X, Y, Z\})$
53	52	eleq2d	$⊢ (φ \land Z = 0_{U}) \to (z \in N (\{X, Y\}) \leftrightarrow z \in N (\{X, Y, Z\}))$
54	53	notbid	$⊢ (φ \land Z = 0_{U}) \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg z \in N (\{X, Y, Z\}))$
55	54	rexbidv	$⊢ (φ \land Z = 0_{U}) \to (\exists z \in V \neg z \in N (\{X, Y\}) \leftrightarrow \exists z \in V \neg z \in N (\{X, Y, Z\}))$
56	44 55	mpbid	$⊢ (φ \land Z = 0_{U}) \to \exists z \in V \neg z \in N (\{X, Y, Z\})$
57	5	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to (K \in HL \land W \in H)$
58	6	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to X \in V$
59	7	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to Y \in V$
60	8	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to Z \in V$
61		simpr1	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to X \neq 0_{U}$
62		simpr2	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to Y \neq 0_{U}$
63		simpr3	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to Z \neq 0_{U}$
64	1 2 3 4 57 58 59 60 11 61 62 63	dvh4dimlem	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U} \land Z \neq 0_{U})) \to \exists z \in V \neg z \in N (\{X, Y, Z\})$
65	26 42 56 64	pm2.61da3ne	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y, Z\})$

Metamath Proof Explorer

Theorem dvh4dimN

Proof