mapdh6kN

Description: Lemmma for mapdh6N . Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh.q	$⊢ Q = 0_{C}$
	mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh.h	$⊢ H = LHyp (K)$
	mapdh.m	$⊢ M = mapd (K) (W)$
	mapdh.u	$⊢ U = DVecH (K) (W)$
	mapdh.v	$⊢ V = {Base}_{U}$
	mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh.n	$⊢ N = LSpan (U)$
	mapdh.c	$⊢ C = LCDual (K) (W)$
	mapdh.d	$⊢ D = {Base}_{C}$
	mapdh.r	$⊢ R = -_{C}$
	mapdh.j	$⊢ J = LSpan (C)$
	mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdhc.f	$⊢ φ \to F \in D$
	mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh.p	$⊢ \underset{˙}{+} = +_{U}$
	mapdh.a	$⊢ \underset{˙}{✚} = +_{C}$
	mapdh6k.y	$⊢ φ \to Y \in V$
	mapdh6k.z	$⊢ φ \to Z \in V$
	mapdh6k.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
Assertion	mapdh6kN	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$⊢ Q = 0_{C}$
2		mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
3		mapdh.h	$⊢ H = LHyp (K)$
4		mapdh.m	$⊢ M = mapd (K) (W)$
5		mapdh.u	$⊢ U = DVecH (K) (W)$
6		mapdh.v	$⊢ V = {Base}_{U}$
7		mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
8		mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
9		mapdh.n	$⊢ N = LSpan (U)$
10		mapdh.c	$⊢ C = LCDual (K) (W)$
11		mapdh.d	$⊢ D = {Base}_{C}$
12		mapdh.r	$⊢ R = -_{C}$
13		mapdh.j	$⊢ J = LSpan (C)$
14		mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdhc.f	$⊢ φ \to F \in D$
16		mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdh.p	$⊢ \underset{˙}{+} = +_{U}$
19		mapdh.a	$⊢ \underset{˙}{✚} = +_{C}$
20		mapdh6k.y	$⊢ φ \to Y \in V$
21		mapdh6k.z	$⊢ φ \to Z \in V$
22		mapdh6k.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
23	14	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to (K \in HL \land W \in H)$
24	15	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to F \in D$
25	16	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to M (N (\{X\})) = J (\{F\})$
26	17	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
27		simpr	$⊢ (φ \land Y = \underset{˙}{0}) \to Y = \underset{˙}{0}$
28	21	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to Z \in V$
29	22	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to \neg X \in N (\{Y, Z\})$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 23 24 25 26 18 19 27 28 29	mapdh6bN	$⊢ (φ \land Y = \underset{˙}{0}) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
31	14	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to (K \in HL \land W \in H)$
32	15	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to F \in D$
33	16	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to M (N (\{X\})) = J (\{F\})$
34	17	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
35	20	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to Y \in V$
36		simpr	$⊢ (φ \land Z = \underset{˙}{0}) \to Z = \underset{˙}{0}$
37	22	adantr	$⊢ (φ \land Z = \underset{˙}{0}) \to \neg X \in N (\{Y, Z\})$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 31 32 33 34 18 19 35 36 37	mapdh6cN	$⊢ (φ \land Z = \underset{˙}{0}) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
39	14	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
40	15	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to F \in D$
41	16	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to M (N (\{X\})) = J (\{F\})$
42	17	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to X \in (V ∖ \{\underset{˙}{0}\})$
43	22	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to \neg X \in N (\{Y, Z\})$
44	20	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Y \in V$
45		simprl	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Y \neq \underset{˙}{0}$
46		eldifsn	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in V \land Y \neq \underset{˙}{0})$
47	44 45 46	sylanbrc	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
48	21	adantr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Z \in V$
49		simprr	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Z \neq \underset{˙}{0}$
50		eldifsn	$⊢ Z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Z \in V \land Z \neq \underset{˙}{0})$
51	48 49 50	sylanbrc	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to Z \in (V ∖ \{\underset{˙}{0}\})$
52	1 2 3 4 5 6 7 8 9 10 11 12 13 39 40 41 42 18 19 43 47 51	mapdh6jN	$⊢ (φ \land (Y \neq \underset{˙}{0} \land Z \neq \underset{˙}{0})) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$
53	30 38 52	pm2.61da2ne	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Metamath Proof Explorer

Theorem mapdh6kN

Proof