mapdh6dN

Description: Lemmma for mapdh6N . (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}$
	mapdh6d.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	mapdh6d.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
	mapdh6d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh6d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdh6d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
	mapdh6d.wn	$⊢ φ \to \neg w \in N (\{X, Y\})$
Assertion	mapdh6dN	$⊢ φ \to I (⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} 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		mapdh6d.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
21		mapdh6d.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
22		mapdh6d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
23		mapdh6d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
24		mapdh6d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
25		mapdh6d.wn	$⊢ φ \to \neg w \in N (\{X, Y\})$
26	3 10 14	lcdlmod	$⊢ φ \to C \in LMod$
27	24	eldifad	$⊢ φ \to w \in V$
28	3 5 14	dvhlvec	$⊢ φ \to U \in LVec$
29	17	eldifad	$⊢ φ \to X \in V$
30	22	eldifad	$⊢ φ \to Y \in V$
31	6 9 28 27 29 30 25	lspindpi	$⊢ φ \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Y\}))$
32	31	simpld	$⊢ φ \to N (\{w\}) \neq N (\{X\})$
33	32	necomd	$⊢ φ \to N (\{X\}) \neq N (\{w\})$
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 27 33	mapdhcl	$⊢ φ \to I (⟨X, F, w⟩) \in D$
35	11 19 1	lmod0vrid	$⊢ (C \in LMod \land I (⟨X, F, w⟩) \in D) \to I (⟨X, F, w⟩) \underset{˙}{✚} Q = I (⟨X, F, w⟩)$
36	26 34 35	syl2anc	$⊢ φ \to I (⟨X, F, w⟩) \underset{˙}{✚} Q = I (⟨X, F, w⟩)$
37	36	adantr	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to I (⟨X, F, w⟩) \underset{˙}{✚} Q = I (⟨X, F, w⟩)$
38		oteq3	$⊢ Y \underset{˙}{+} Z = \underset{˙}{0} \to ⟨X, F, Y \underset{˙}{+} Z⟩ = ⟨X, F, \underset{˙}{0}⟩$
39	38	fveq2d	$⊢ Y \underset{˙}{+} Z = \underset{˙}{0} \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, \underset{˙}{0}⟩)$
40	1 2 8 17 15	mapdhval0	$⊢ φ \to I (⟨X, F, \underset{˙}{0}⟩) = Q$
41	39 40	sylan9eqr	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = Q$
42	41	oveq2d	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} Q$
43		oveq2	$⊢ Y \underset{˙}{+} Z = \underset{˙}{0} \to w \underset{˙}{+} (Y \underset{˙}{+} Z) = w \underset{˙}{+} \underset{˙}{0}$
44	3 5 14	dvhlmod	$⊢ φ \to U \in LMod$
45	6 18 8	lmod0vrid	$⊢ (U \in LMod \land w \in V) \to w \underset{˙}{+} \underset{˙}{0} = w$
46	44 27 45	syl2anc	$⊢ φ \to w \underset{˙}{+} \underset{˙}{0} = w$
47	43 46	sylan9eqr	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to w \underset{˙}{+} (Y \underset{˙}{+} Z) = w$
48	47	oteq3d	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to ⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩ = ⟨X, F, w⟩$
49	48	fveq2d	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to I (⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩) = I (⟨X, F, w⟩)$
50	37 42 49	3eqtr4rd	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to I (⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩)$
51	14	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
52	15	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to F \in D$
53	16	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to M (N (\{X\})) = J (\{F\})$
54	17	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
55	24	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to w \in (V ∖ \{\underset{˙}{0}\})$
56	23	eldifad	$⊢ φ \to Z \in V$
57	6 18	lmodvacl	$⊢ (U \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
58	44 30 56 57	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
59	58	anim1i	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to (Y \underset{˙}{+} Z \in V \land Y \underset{˙}{+} Z \neq \underset{˙}{0})$
60		eldifsn	$⊢ Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \underset{˙}{+} Z \in V \land Y \underset{˙}{+} Z \neq \underset{˙}{0})$
61	59 60	sylibr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\})$
62	6 9 28 29 30 56 20	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
63	62	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
64	6 18 8 9 28 17 22 23 24 21 63 25	mapdindp1	$⊢ φ \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$
65	6 18 8 9 28 17 22 23 24 21 63 25	mapdindp2	$⊢ φ \to \neg w \in N (\{X, Y \underset{˙}{+} Z\})$
66	6 8 9 28 17 58 27 64 65	lspindp1	$⊢ φ \to (N (\{w\}) \neq N (\{Y \underset{˙}{+} Z\}) \land \neg X \in N (\{w, Y \underset{˙}{+} Z\}))$
67	66	simprd	$⊢ φ \to \neg X \in N (\{w, Y \underset{˙}{+} Z\})$
68	67	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to \neg X \in N (\{w, Y \underset{˙}{+} Z\})$
69	31	simprd	$⊢ φ \to N (\{w\}) \neq N (\{Y\})$
70	6 8 9 28 24 30 69	lspsnne1	$⊢ φ \to \neg w \in N (\{Y\})$
71		eqid	$⊢ LSSum (U) = LSSum (U)$
72	6 9 71 44 30 56	lsmpr	$⊢ φ \to N (\{Y, Z\}) = N (\{Y\}) LSSum (U) N (\{Z\})$
73	21	oveq2d	$⊢ φ \to N (\{Y\}) LSSum (U) N (\{Y\}) = N (\{Y\}) LSSum (U) N (\{Z\})$
74		eqid	$⊢ LSubSp (U) = LSubSp (U)$
75	6 74 9	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
76	44 30 75	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
77	74	lsssubg	$⊢ (U \in LMod \land N (\{Y\}) \in LSubSp (U)) \to N (\{Y\}) \in SubGrp (U)$
78	44 76 77	syl2anc	$⊢ φ \to N (\{Y\}) \in SubGrp (U)$
79	71	lsmidm	$⊢ N (\{Y\}) \in SubGrp (U) \to N (\{Y\}) LSSum (U) N (\{Y\}) = N (\{Y\})$
80	78 79	syl	$⊢ φ \to N (\{Y\}) LSSum (U) N (\{Y\}) = N (\{Y\})$
81	72 73 80	3eqtr2d	$⊢ φ \to N (\{Y, Z\}) = N (\{Y\})$
82	70 81	neleqtrrd	$⊢ φ \to \neg w \in N (\{Y, Z\})$
83	6 18 9 44 30 56 27 82	lspindp4	$⊢ φ \to \neg w \in N (\{Y, Y \underset{˙}{+} Z\})$
84	6 9 28 27 30 58 83	lspindpi	$⊢ φ \to (N (\{w\}) \neq N (\{Y\}) \land N (\{w\}) \neq N (\{Y \underset{˙}{+} Z\}))$
85	84	simprd	$⊢ φ \to N (\{w\}) \neq N (\{Y \underset{˙}{+} Z\})$
86	85	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to N (\{w\}) \neq N (\{Y \underset{˙}{+} Z\})$
87		eqidd	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to I (⟨X, F, w⟩) = I (⟨X, F, w⟩)$
88		eqidd	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y \underset{˙}{+} Z⟩)$
89	1 2 3 4 5 6 7 8 9 10 11 12 13 51 52 53 54 18 19 55 61 68 86 87 88	mapdh6aN	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to I (⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩)$
90	50 89	pm2.61dane	$⊢ φ \to I (⟨X, F, w \underset{˙}{+} (Y \underset{˙}{+} Z)⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩)$

Metamath Proof Explorer

Theorem mapdh6dN

Proof