Theorem hdmap11lem1

Description: Lemma for hdmapadd . (Contributed by NM, 26-May-2015)

	Ref	Expression
Hypotheses	hdmap11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap11.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap11.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap11.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap11.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap11.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap11.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap11.x	$$⊢\phi \to X\in V$$
	hdmap11.y	$$⊢\phi \to Y\in V$$
	hdmap11.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmap11.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap11.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap11.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap11.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap11.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap11.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hdmap11.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap11lem0.1a	$$⊢\phi \to z\in V$$
	hdmap11lem0.6	$$⊢\phi \to \neg z\in N\left(\left\{X,Y\right\}\right)$$
	hdmap11lem0.2a	$$⊢\phi \to N\left(\left\{z\right\}\right)\ne N\left(\left\{E\right\}\right)$$
Assertion	hdmap11lem1	$$⊢\phi \to S\left(X\underset{\dot{}}{+}Y\right)=S\left(X\right)\underset{\dot{}}{✚}S\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap11.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap11.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap11.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap11.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap11.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
7		hdmap11.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmap11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmap11.x	$$⊢\phi \to X\in V$$
10		hdmap11.y	$$⊢\phi \to Y\in V$$
11		hdmap11.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
12		hdmap11.o	$$⊢\underset{\dot{}}{0}=0_U$$
13		hdmap11.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
14		hdmap11.d	$$⊢D={\mathrm{Base}}_C$$
15		hdmap11.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
16		hdmap11.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
17		hdmap11.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
18		hdmap11.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
19		hdmap11lem0.1a	$$⊢\phi \to z\in V$$
20		hdmap11lem0.6	$$⊢\phi \to \neg z\in N\left(\left\{X,Y\right\}\right)$$
21		hdmap11lem0.2a	$$⊢\phi \to N\left(\left\{z\right\}\right)\ne N\left(\left\{E\right\}\right)$$
22		eqid	$$⊢0_C=0_C$$
23		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
24		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
25	1 23 24 2 3 12 11 8	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
26	1 2 3 12 5 14 22 17 8 25	hvmapcl2	$$⊢\phi \to J\left(E\right)\in \left(D\setminus \left\{0_C\right\}\right)$$
27	26	eldifad	$$⊢\phi \to J\left(E\right)\in D$$
28	1 2 3 12 13 5 15 16 17 8 25	mapdhvmap	$$⊢\phi \to M\left(N\left(\left\{E\right\}\right)\right)=L\left(\left\{J\left(E\right)\right\}\right)$$
29	21	necomd	$$⊢\phi \to N\left(\left\{E\right\}\right)\ne N\left(\left\{z\right\}\right)$$
30	1 2 3 12 13 5 14 15 16 18 8 27 28 29 25 19	hdmap1cl	$$⊢\phi \to I\left(⟨E,J\left(E\right),z⟩\right)\in D$$
31		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
32	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
33	3 31 13 32 9 10	lspprcl	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
34	12 31 32 33 19 20	lssneln0	$$⊢\phi \to z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
35		eqidd	$$⊢\phi \to I\left(⟨E,J\left(E\right),z⟩\right)=I\left(⟨E,J\left(E\right),z⟩\right)$$
36		eqid	$$⊢{-}_U={-}_U$$
37		eqid	$$⊢{-}_C={-}_C$$
38	1 2 3 36 12 13 5 14 37 15 16 18 8 25 27 34 30 29 28	hdmap1eq	$$⊢\phi \to \left(I\left(⟨E,J\left(E\right),z⟩\right)=I\left(⟨E,J\left(E\right),z⟩\right)\leftrightarrow \left(M\left(N\left(\left\{z\right\}\right)\right)=L\left(\left\{I\left(⟨E,J\left(E\right),z⟩\right)\right\}\right)\wedge M\left(N\left(\left\{E{-}_{U}z\right\}\right)\right)=L\left(\left\{J\left(E\right){-}_{C}I\left(⟨E,J\left(E\right),z⟩\right)\right\}\right)\right)\right)$$
39	35 38	mpbid	$$⊢\phi \to \left(M\left(N\left(\left\{z\right\}\right)\right)=L\left(\left\{I\left(⟨E,J\left(E\right),z⟩\right)\right\}\right)\wedge M\left(N\left(\left\{E{-}_{U}z\right\}\right)\right)=L\left(\left\{J\left(E\right){-}_{C}I\left(⟨E,J\left(E\right),z⟩\right)\right\}\right)\right)$$
40	39	simpld	$$⊢\phi \to M\left(N\left(\left\{z\right\}\right)\right)=L\left(\left\{I\left(⟨E,J\left(E\right),z⟩\right)\right\}\right)$$
41	1 2 3 4 12 13 5 14 6 15 16 18 8 30 34 9 10 20 40	hdmap1l6	$$⊢\phi \to I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),X\underset{\dot{}}{+}Y⟩\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),X⟩\right)\underset{\dot{}}{✚}I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),Y⟩\right)$$
42	3 4	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{+}Y\in V$$
43	32 9 10 42	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in V$$
44	1 2 8	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
45	25	eldifad	$$⊢\phi \to E\in V$$
46	3 4 13 32 9 10	lspprvacl	$$⊢\phi \to X\underset{\dot{}}{+}Y\in N\left(\left\{X,Y\right\}\right)$$
47	31 13 32 33 46	lspsnel5a	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
48	47 20	ssneldd	$$⊢\phi \to \neg z\in N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
49	3 13 32 19 43 48	lspsnne2	$$⊢\phi \to N\left(\left\{z\right\}\right)\ne N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
50	3 13 12 44 45 43 34 21 49	hdmaplem4	$$⊢\phi \to \neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)$$
51	1 11 2 3 13 5 14 17 18 7 8 43 19 50	hdmapval2	$$⊢\phi \to S\left(X\underset{\dot{}}{+}Y\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),X\underset{\dot{}}{+}Y⟩\right)$$
52	3 13 44 19 9 10 20	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\{Y\right\}\right)\right)$$
53	52	simpld	$$⊢\phi \to N\left(\left\{z\right\}\right)\ne N\left(\left\{X\right\}\right)$$
54	3 13 12 44 45 9 34 21 53	hdmaplem4	$$⊢\phi \to \neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{X\right\}\right)\right)$$
55	1 11 2 3 13 5 14 17 18 7 8 9 19 54	hdmapval2	$$⊢\phi \to S\left(X\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),X⟩\right)$$
56	52	simprd	$$⊢\phi \to N\left(\left\{z\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
57	3 13 12 44 45 10 34 21 56	hdmaplem4	$$⊢\phi \to \neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{Y\right\}\right)\right)$$
58	1 11 2 3 13 5 14 17 18 7 8 10 19 57	hdmapval2	$$⊢\phi \to S\left(Y\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),Y⟩\right)$$
59	55 58	oveq12d	$$⊢\phi \to S\left(X\right)\underset{\dot{}}{✚}S\left(Y\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),X⟩\right)\underset{\dot{}}{✚}I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),Y⟩\right)$$
60	41 51 59	3eqtr4d	$$⊢\phi \to S\left(X\underset{\dot{}}{+}Y\right)=S\left(X\right)\underset{\dot{}}{✚}S\left(Y\right)$$