Theorem hdmap1l6e

Description: Lemmma for hdmap1l6 . Part (6) in Baer p. 47 line 38. (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	hdmap1l6e	$$⊢\phi \to I\left(⟨X,F,\left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,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 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
27	24	eldifad	$$⊢\phi \to w\in V$$
28	22	eldifad	$$⊢\phi \to Y\in V$$
29	3 4	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge w\in V\wedge Y\in V\right)\to w\underset{\dot{}}{+}Y\in V$$
30	26 27 28 29	syl3anc	$$⊢\phi \to w\underset{\dot{}}{+}Y\in V$$
31	1 2 16	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
32	18	eldifad	$$⊢\phi \to X\in V$$
33	3 7 31 27 32 28 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)$$
34	33	simprd	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
35	3 4 6 7 26 27 28 34	lmodindp1	$$⊢\phi \to w\underset{\dot{}}{+}Y\ne \underset{\dot{}}{0}$$
36		eldifsn	$$⊢w\underset{\dot{}}{+}Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(w\underset{\dot{}}{+}Y\in V\wedge w\underset{\dot{}}{+}Y\ne \underset{\dot{}}{0}\right)$$
37	30 35 36	sylanbrc	$$⊢\phi \to w\underset{\dot{}}{+}Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
38	23	eldifad	$$⊢\phi \to Z\in V$$
39	3 7 31 32 28 38 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)$$
40	39	simpld	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
41	3 4 6 7 31 18 22 23 24 21 40 25	mapdindp3	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
42	3 4 6 7 31 18 22 23 24 21 40 25	mapdindp4	$$⊢\phi \to \neg Z\in N\left(\left\{X,w\underset{\dot{}}{+}Y\right\}\right)$$
43	3 6 7 31 18 30 38 41 42	lspindp1	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\wedge \neg X\in N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)\right)$$
44	43	simprd	$$⊢\phi \to \neg X\in N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)$$
45		prcom	$$⊢\left\{w\underset{\dot{}}{+}Y,Z\right\}=\left\{Z,w\underset{\dot{}}{+}Y\right\}$$
46	45	fveq2i	$$⊢N\left(\left\{w\underset{\dot{}}{+}Y,Z\right\}\right)=N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)$$
47	46	eleq2i	$$⊢X\in N\left(\left\{w\underset{\dot{}}{+}Y,Z\right\}\right)\leftrightarrow X\in N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)$$
48	44 47	sylnibr	$$⊢\phi \to \neg X\in N\left(\left\{w\underset{\dot{}}{+}Y,Z\right\}\right)$$
49	3 7 31 38 32 30 42	lspindpi	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge N\left(\left\{Z\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\right)$$
50	49	simprd	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
51	50	necomd	$$⊢\phi \to N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
52		eqidd	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)=I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)$$
53		eqidd	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)=I\left(⟨X,F,Z⟩\right)$$
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 37 23 48 51 52 53	hdmap1l6a	$$⊢\phi \to I\left(⟨X,F,\left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$