dvh3dim2

Description: There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-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$
	dvh3dim2.z	$⊢ φ \to Z \in V$
Assertion	dvh3dim2	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, 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 6 8	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Z\})$
10	9	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to \exists z \in V \neg z \in N (\{X, Z\})$
11		eqid	$⊢ LSubSp (U) = LSubSp (U)$
12	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
13	12	ad2antrr	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to U \in LMod$
14	3 11 4 12 6 8	lspprcl	$⊢ φ \to N (\{X, Z\}) \in LSubSp (U)$
15	14	ad2antrr	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to N (\{X, Z\}) \in LSubSp (U)$
16	3 4 12 6 8	lspprid1	$⊢ φ \to X \in N (\{X, Z\})$
17	16	ad2antrr	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to X \in N (\{X, Z\})$
18		simplr	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to Y \in N (\{X, Z\})$
19	11 4 13 15 17 18	lspprss	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to N (\{X, Y\}) \subseteq N (\{X, Z\})$
20	19	ssneld	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to (\neg z \in N (\{X, Z\}) \to \neg z \in N (\{X, Y\}))$
21	20	ancrd	$⊢ ((φ \land Y \in N (\{X, Z\})) \land z \in V) \to (\neg z \in N (\{X, Z\}) \to (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\})))$
22	21	reximdva	$⊢ (φ \land Y \in N (\{X, Z\})) \to (\exists z \in V \neg z \in N (\{X, Z\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\})))$
23	10 22	mpd	$⊢ (φ \land Y \in N (\{X, Z\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
24	1 2 3 4 5 6 7	dvh3dim	$⊢ φ \to \exists w \in V \neg w \in N (\{X, Y\})$
25	24	adantr	$⊢ (φ \land \neg Y \in N (\{X, Z\})) \to \exists w \in V \neg w \in N (\{X, Y\})$
26		simpl1l	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to φ$
27	26 12	syl	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to U \in LMod$
28		simpl2	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to w \in V$
29	26 7	syl	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to Y \in V$
30		eqid	$⊢ +_{U} = +_{U}$
31	3 30	lmodvacl	$⊢ (U \in LMod \land w \in V \land Y \in V) \to w +_{U} Y \in V$
32	27 28 29 31	syl3anc	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to w +_{U} Y \in V$
33	3 11 4 12 6 7	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
34	26 33	syl	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to N (\{X, Y\}) \in LSubSp (U)$
35	3 4 12 6 7	lspprid2	$⊢ φ \to Y \in N (\{X, Y\})$
36	26 35	syl	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to Y \in N (\{X, Y\})$
37		simpl3	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to \neg w \in N (\{X, Y\})$
38	3 30 11 27 34 36 28 37	lssvancl2	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to \neg w +_{U} Y \in N (\{X, Y\})$
39	26 14	syl	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to N (\{X, Z\}) \in LSubSp (U)$
40		simpr	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to w \in N (\{X, Z\})$
41		simpl1r	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to \neg Y \in N (\{X, Z\})$
42	3 30 11 27 39 40 29 41	lssvancl1	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to \neg w +_{U} Y \in N (\{X, Z\})$
43		eleq1	$⊢ z = w +_{U} Y \to (z \in N (\{X, Y\}) \leftrightarrow w +_{U} Y \in N (\{X, Y\}))$
44	43	notbid	$⊢ z = w +_{U} Y \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg w +_{U} Y \in N (\{X, Y\}))$
45		eleq1	$⊢ z = w +_{U} Y \to (z \in N (\{X, Z\}) \leftrightarrow w +_{U} Y \in N (\{X, Z\}))$
46	45	notbid	$⊢ z = w +_{U} Y \to (\neg z \in N (\{X, Z\}) \leftrightarrow \neg w +_{U} Y \in N (\{X, Z\}))$
47	44 46	anbi12d	$⊢ z = w +_{U} Y \to ((\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\})) \leftrightarrow (\neg w +_{U} Y \in N (\{X, Y\}) \land \neg w +_{U} Y \in N (\{X, Z\})))$
48	47	rspcev	$⊢ (w +_{U} Y \in V \land (\neg w +_{U} Y \in N (\{X, Y\}) \land \neg w +_{U} Y \in N (\{X, Z\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
49	32 38 42 48	syl12anc	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land w \in N (\{X, Z\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
50		simpl2	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land \neg w \in N (\{X, Z\})) \to w \in V$
51		simpl3	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land \neg w \in N (\{X, Z\})) \to \neg w \in N (\{X, Y\})$
52		simpr	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land \neg w \in N (\{X, Z\})) \to \neg w \in N (\{X, Z\})$
53		eleq1	$⊢ z = w \to (z \in N (\{X, Y\}) \leftrightarrow w \in N (\{X, Y\}))$
54	53	notbid	$⊢ z = w \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg w \in N (\{X, Y\}))$
55		eleq1	$⊢ z = w \to (z \in N (\{X, Z\}) \leftrightarrow w \in N (\{X, Z\}))$
56	55	notbid	$⊢ z = w \to (\neg z \in N (\{X, Z\}) \leftrightarrow \neg w \in N (\{X, Z\}))$
57	54 56	anbi12d	$⊢ z = w \to ((\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\})) \leftrightarrow (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\})))$
58	57	rspcev	$⊢ (w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
59	50 51 52 58	syl12anc	$⊢ (((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \land \neg w \in N (\{X, Z\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
60	49 59	pm2.61dan	$⊢ ((φ \land \neg Y \in N (\{X, Z\})) \land w \in V \land \neg w \in N (\{X, Y\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
61	60	rexlimdv3a	$⊢ (φ \land \neg Y \in N (\{X, Z\})) \to (\exists w \in V \neg w \in N (\{X, Y\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\})))$
62	25 61	mpd	$⊢ (φ \land \neg Y \in N (\{X, Z\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$
63	23 62	pm2.61dan	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{X, Z\}))$

Metamath Proof Explorer

Theorem dvh3dim2

Proof