Theorem hdmap1l6d

Description: Lemmma for hdmap1l6 . (Contributed by NM, 1-May-2015)

	Ref	Expression
Hypotheses	hdmap1l6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1l6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1l6.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1l6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap1l6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap1l6c.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1l6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1l6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1l6.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1l6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap1l6.r	$$⊢R={-}_C$$
	hdmap1l6.q	$$⊢Q=0_C$$
	hdmap1l6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap1l6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1l6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1l6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1l6.f	$$⊢\phi \to F\in D$$
	hdmap1l6cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
	hdmap1l6d.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	hdmap1l6d.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
	hdmap1l6d.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6d.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6d.w	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6d.wn	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\right\}\right)$$
Assertion	hdmap1l6d	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1l6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1l6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1l6.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1l6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap1l6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		hdmap1l6c.o	$$⊢\underset{\dot{}}{0}=0_U$$
7		hdmap1l6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		hdmap1l6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		hdmap1l6.d	$$⊢D={\mathrm{Base}}_C$$
10		hdmap1l6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
11		hdmap1l6.r	$$⊢R={-}_C$$
12		hdmap1l6.q	$$⊢Q=0_C$$
13		hdmap1l6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
14		hdmap1l6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
15		hdmap1l6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
16		hdmap1l6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hdmap1l6.f	$$⊢\phi \to F\in D$$
18		hdmap1l6cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		hdmap1l6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
20		hdmap1l6d.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
21		hdmap1l6d.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
22		hdmap1l6d.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
23		hdmap1l6d.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24		hdmap1l6d.w	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25		hdmap1l6d.wn	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\right\}\right)$$
26	1 8 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
27	1 2 16	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
28	24	eldifad	$$⊢\phi \to w\in V$$
29	18	eldifad	$$⊢\phi \to X\in V$$
30	22	eldifad	$$⊢\phi \to Y\in V$$
31	3 7 27 28 29 30 25	lspindpi	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
32	31	simpld	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{X\right\}\right)$$
33	32	necomd	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{w\right\}\right)$$
34	1 2 3 6 7 8 9 13 14 15 16 17 19 33 18 28	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,w⟩\right)\in D$$
35	9 10 12	lmod0vrid	$$⊢\left(C\in \mathrm{LMod}\wedge I\left(⟨X,F,w⟩\right)\in D\right)\to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}Q=I\left(⟨X,F,w⟩\right)$$
36	26 34 35	syl2anc	$$⊢\phi \to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}Q=I\left(⟨X,F,w⟩\right)$$
37	36	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}Q=I\left(⟨X,F,w⟩\right)$$
38		oteq3	$$⊢Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\to ⟨X,F,Y\underset{\dot{}}{+}Z⟩=⟨X,F,\underset{\dot{}}{0}⟩$$
39	38	fveq2d	$$⊢Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)$$
40	1 2 3 6 8 9 12 15 16 17 29	hdmap1val0	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)=Q$$
41	39 40	sylan9eqr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=Q$$
42	41	oveq2d	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}Q$$
43		oveq2	$$⊢Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\to w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=w\underset{\dot{}}{+}\underset{\dot{}}{0}$$
44	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
45	3 4 6	lmod0vrid	$$⊢\left(U\in \mathrm{LMod}\wedge w\in V\right)\to w\underset{\dot{}}{+}\underset{\dot{}}{0}=w$$
46	44 28 45	syl2anc	$$⊢\phi \to w\underset{\dot{}}{+}\underset{\dot{}}{0}=w$$
47	43 46	sylan9eqr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=w$$
48	47	oteq3d	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to ⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩=⟨X,F,w⟩$$
49	48	fveq2d	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)$$
50	37 42 49	3eqtr4rd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$
51	16	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
52	17	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to F\in D$$
53	18	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
54	19	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
55	24	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
56	23	eldifad	$$⊢\phi \to Z\in V$$
57	3 4	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
58	44 30 56 57	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
59	58	anim1i	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to \left(Y\underset{\dot{}}{+}Z\in V\wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)$$
60		eldifsn	$$⊢Y\underset{\dot{}}{+}Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Y\underset{\dot{}}{+}Z\in V\wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)$$
61	59 60	sylibr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to Y\underset{\dot{}}{+}Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
62	3 7 27 29 30 56 20	lspindpi	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)\right)$$
63	62	simpld	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
64	3 4 6 7 27 18 22 23 24 21 63 25	mapdindp1	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
65	3 4 6 7 27 18 22 23 24 21 63 25	mapdindp2	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)$$
66	3 6 7 27 18 58 28 64 65	lspindp1	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\wedge \neg X\in N\left(\left\{w,Y\underset{\dot{}}{+}Z\right\}\right)\right)$$
67	66	simprd	$$⊢\phi \to \neg X\in N\left(\left\{w,Y\underset{\dot{}}{+}Z\right\}\right)$$
68	67	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to \neg X\in N\left(\left\{w,Y\underset{\dot{}}{+}Z\right\}\right)$$
69	31	simprd	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
70	3 6 7 27 24 30 69	lspsnne1	$$⊢\phi \to \neg w\in N\left(\left\{Y\right\}\right)$$
71		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
72	3 7 71 44 30 56	lsmpr	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)=N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Z\right\}\right)$$
73	21	oveq2d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)=N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Z\right\}\right)$$
74		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
75	3 74 7	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
76	44 30 75	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
77	74	lsssubg	$$⊢\left(U\in \mathrm{LMod}\wedge N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(U\right)$$
78	44 76 77	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(U\right)$$
79	71	lsmidm	$$⊢N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(U\right)\to N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)=N\left(\left\{Y\right\}\right)$$
80	78 79	syl	$$⊢\phi \to N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)=N\left(\left\{Y\right\}\right)$$
81	72 73 80	3eqtr2d	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)=N\left(\left\{Y\right\}\right)$$
82	70 81	neleqtrrd	$$⊢\phi \to \neg w\in N\left(\left\{Y,Z\right\}\right)$$
83	3 4 7 44 30 56 28 82	lspindp4	$$⊢\phi \to \neg w\in N\left(\left\{Y,Y\underset{\dot{}}{+}Z\right\}\right)$$
84	3 7 27 28 30 58 83	lspindpi	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)$$
85	84	simprd	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
86	85	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
87		eqidd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to I\left(⟨X,F,w⟩\right)=I\left(⟨X,F,w⟩\right)$$
88		eqidd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$
89	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 51 52 53 54 55 61 68 86 87 88	hdmap1l6a	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$
90	50 89	pm2.61dane	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$