Theorem hdmap1l6a

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, case 1. (Contributed by NM, 23-Apr-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)$$
	hdmap1l6e.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6e.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6e.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	hdmap1l6.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
	hdmap1l6.fg	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
	hdmap1l6.fe	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)=E$$
Assertion	hdmap1l6a	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,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		hdmap1l6e.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
21		hdmap1l6e.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
22		hdmap1l6e.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
23		hdmap1l6.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
24		hdmap1l6.fg	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
25		hdmap1l6.fe	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)=E$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	hdmap1l6lem2	$$⊢\phi \to M\left(N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)=L\left(\left\{G\underset{\dot{}}{✚}E\right\}\right)$$
27	24 25	oveq12d	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)=G\underset{\dot{}}{✚}E$$
28	27	sneqd	$$⊢\phi \to \left\{I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right\}=\left\{G\underset{\dot{}}{✚}E\right\}$$
29	28	fveq2d	$$⊢\phi \to L\left(\left\{I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right\}\right)=L\left(\left\{G\underset{\dot{}}{✚}E\right\}\right)$$
30	26 29	eqtr4d	$$⊢\phi \to M\left(N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)=L\left(\left\{I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right\}\right)$$
31	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	hdmap1l6lem1	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)=L\left(\left\{FR\left(G\underset{\dot{}}{✚}E\right)\right\}\right)$$
32	27	oveq2d	$$⊢\phi \to FR\left(I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right)=FR\left(G\underset{\dot{}}{✚}E\right)$$
33	32	sneqd	$$⊢\phi \to \left\{FR\left(I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right)\right\}=\left\{FR\left(G\underset{\dot{}}{✚}E\right)\right\}$$
34	33	fveq2d	$$⊢\phi \to L\left(\left\{FR\left(I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right)\right\}\right)=L\left(\left\{FR\left(G\underset{\dot{}}{✚}E\right)\right\}\right)$$
35	31 34	eqtr4d	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)=L\left(\left\{FR\left(I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right)\right\}\right)$$
36	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
37	20	eldifad	$$⊢\phi \to Y\in V$$
38	21	eldifad	$$⊢\phi \to Z\in V$$
39	3 4	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
40	36 37 38 39	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
41	3 4 6 7 36 37 38 23	lmodindp1	$$⊢\phi \to Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}$$
42		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)$$
43	40 41 42	sylanbrc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
44	1 8 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
45	1 2 16	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
46	18	eldifad	$$⊢\phi \to X\in V$$
47	3 6 7 45 37 21 46 23 22	lspindp2	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge \neg Z\in N\left(\left\{X,Y\right\}\right)\right)$$
48	47	simpld	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
49	1 2 3 6 7 8 9 13 14 15 16 17 19 48 18 37	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$
50	3 6 7 45 20 38 46 23 22	lspindp1	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)\wedge \neg Y\in N\left(\left\{X,Z\right\}\right)\right)$$
51	50	simpld	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
52	1 2 3 6 7 8 9 13 14 15 16 17 19 51 18 38	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)\in D$$
53	9 10	lmodvacl	$$⊢\left(C\in \mathrm{LMod}\wedge I\left(⟨X,F,Y⟩\right)\in D\wedge I\left(⟨X,F,Z⟩\right)\in D\right)\to I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\in D$$
54	44 49 52 53	syl3anc	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\in D$$
55		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
56	3 55 7 36 37 38	lspprcl	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
57	3 4 7 36 37 38	lspprvacl	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in N\left(\left\{Y,Z\right\}\right)$$
58	55 7 36 56 57	lspsnel5a	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)$$
59	3 55 7 36 56 46	lspsnel5	$$⊢\phi \to \left(X\in N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)\right)$$
60	22 59	mtbid	$$⊢\phi \to \neg N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)$$
61		nssne2	$$⊢\left(N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)\wedge \neg N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)\right)\to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\ne N\left(\left\{X\right\}\right)$$
62	58 60 61	syl2anc	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\ne N\left(\left\{X\right\}\right)$$
63	62	necomd	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
64	1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 43 54 63 19	hdmap1eq	$$⊢\phi \to \left(I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\leftrightarrow \left(M\left(N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)=L\left(\left\{I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)=L\left(\left\{FR\left(I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)\right)\right\}\right)\right)\right)$$
65	30 35 64	mpbir2and	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$