Theorem hdmapeveclem

Description: Lemma for hdmapevec . TODO: combine with hdmapevec if it shortens overall. (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmapevec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapevec.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapevec.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hdmapevec.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapevec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapevec.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapevec.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapevec.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmapevec.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmapevec.d	$$⊢D={\mathrm{Base}}_C$$
	hdmapevec.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmapevec.x	$$⊢\phi \to X\in V$$
	hdmapevec.ne	$$⊢\phi \to \neg X\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{E\right\}\right)\right)$$
Assertion	hdmapeveclem	$$⊢\phi \to S\left(E\right)=J\left(E\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapevec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapevec.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapevec.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
4		hdmapevec.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
5		hdmapevec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		hdmapevec.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
7		hdmapevec.v	$$⊢V={\mathrm{Base}}_U$$
8		hdmapevec.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
9		hdmapevec.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
10		hdmapevec.d	$$⊢D={\mathrm{Base}}_C$$
11		hdmapevec.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
12		hdmapevec.x	$$⊢\phi \to X\in V$$
13		hdmapevec.ne	$$⊢\phi \to \neg X\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{E\right\}\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
15		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
16		eqid	$$⊢0_U=0_U$$
17	1 14 15 6 7 16 2 5	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
18	17	eldifad	$$⊢\phi \to E\in V$$
19	1 2 6 7 8 9 10 3 11 4 5 18 12 13	hdmapval2	$$⊢\phi \to S\left(E\right)=I\left(⟨X,I\left(⟨E,J\left(E\right),X⟩\right),E⟩\right)$$
20		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
21		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
22		eqid	$$⊢0_C=0_C$$
23	1 6 7 16 9 10 22 3 5 17	hvmapcl2	$$⊢\phi \to J\left(E\right)\in \left(D\setminus \left\{0_C\right\}\right)$$
24	23	eldifad	$$⊢\phi \to J\left(E\right)\in D$$
25	1 6 7 16 8 9 20 21 3 5 17	mapdhvmap	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{E\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{J\left(E\right)\right\}\right)$$
26	1 6 5	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
27	7 8 26 12 13 18	hdmaplem1	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{E\right\}\right)$$
28	27	necomd	$$⊢\phi \to N\left(\left\{E\right\}\right)\ne N\left(\left\{X\right\}\right)$$
29	7 8 26 12 13 18 16	hdmaplem3	$$⊢\phi \to X\in \left(V\setminus \left\{0_U\right\}\right)$$
30		eqidd	$$⊢\phi \to I\left(⟨E,J\left(E\right),X⟩\right)=I\left(⟨E,J\left(E\right),X⟩\right)$$
31	1 6 7 16 8 9 10 20 21 11 5 24 25 28 17 29 30	hdmap1eq2	$$⊢\phi \to I\left(⟨X,I\left(⟨E,J\left(E\right),X⟩\right),E⟩\right)=J\left(E\right)$$
32	19 31	eqtrd	$$⊢\phi \to S\left(E\right)=J\left(E\right)$$