Theorem hdmapffval

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypothesis	hdmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	hdmapffval	$$⊢K\in X\to \mathrm{HDMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		elex	$$⊢K\in X\to K\in \mathrm{V}$$
3		fveq2	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=\mathrm{LHyp}\left(K\right)$$
4	3 1	eqtr4di	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=H$$
5		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
6	5	reseq2d	$$⊢k=K\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k}={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}$$
7		fveq2	$$⊢k=K\to \mathrm{LTrn}\left(k\right)=\mathrm{LTrn}\left(K\right)$$
8	7	fveq1d	$$⊢k=K\to \mathrm{LTrn}\left(k\right)\left(w\right)=\mathrm{LTrn}\left(K\right)\left(w\right)$$
9	8	reseq2d	$$⊢k=K\to {\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}={\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}$$
10	6 9	opeq12d	$$⊢k=K\to ⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩$$
11		fveq2	$$⊢k=K\to \mathrm{DVecH}\left(k\right)=\mathrm{DVecH}\left(K\right)$$
12	11	fveq1d	$$⊢k=K\to \mathrm{DVecH}\left(k\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(w\right)$$
13		fveq2	$$⊢k=K\to \mathrm{HDMap1}\left(k\right)=\mathrm{HDMap1}\left(K\right)$$
14	13	fveq1d	$$⊢k=K\to \mathrm{HDMap1}\left(k\right)\left(w\right)=\mathrm{HDMap1}\left(K\right)\left(w\right)$$
15		fveq2	$$⊢k=K\to \mathrm{LCDual}\left(k\right)=\mathrm{LCDual}\left(K\right)$$
16	15	fveq1d	$$⊢k=K\to \mathrm{LCDual}\left(k\right)\left(w\right)=\mathrm{LCDual}\left(K\right)\left(w\right)$$
17	16	fveq2d	$$⊢k=K\to {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}$$
18		fveq2	$$⊢k=K\to \mathrm{HVMap}\left(k\right)=\mathrm{HVMap}\left(K\right)$$
19	18	fveq1d	$$⊢k=K\to \mathrm{HVMap}\left(k\right)\left(w\right)=\mathrm{HVMap}\left(K\right)\left(w\right)$$
20	19	fveq1d	$$⊢k=K\to \mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right)=\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right)$$
21	20	oteq2d	$$⊢k=K\to ⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩=⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩$$
22	21	fveq2d	$$⊢k=K\to i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right)=i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right)$$
23	22	oteq2d	$$⊢k=K\to ⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩=⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩$$
24	23	fveq2d	$$⊢k=K\to i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)$$
25	24	eqeq2d	$$⊢k=K\to \left(y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\leftrightarrow y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)$$
26	25	imbi2d	$$⊢k=K\to \left(\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\leftrightarrow \left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)$$
27	26	ralbidv	$$⊢k=K\to \left(\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\leftrightarrow \forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)$$
28	17 27	riotaeqbidv	$$⊢k=K\to \left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)=\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)$$
29	28	mpteq2dv	$$⊢k=K\to \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)=\left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)$$
30	29	eleq2d	$$⊢k=K\to \left(a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\leftrightarrow a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right)$$
31	14 30	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right)$$
32	31	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right)$$
33	12 32	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right)$$
34	10 33	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right)$$
35	34	abbidv	$$⊢k=K\to \left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}=\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}$$
36	4 35	mpteq12dv	$$⊢k=K\to \left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)$$
37		df-hdmap	$$⊢\mathrm{HDMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(k\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)\right)$$
38	36 37 1	mptfvmpt	$$⊢K\in \mathrm{V}\to \mathrm{HDMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)$$
39	2 38	syl	$$⊢K\in X\to \mathrm{HDMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(w\right)}⟩/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap1}\left(K\right)\left(w\right)/i\underset{\dot{}}{]}a\in \left(t\in v⟼\left(\iota y\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(w\right)}|\forall z\in v\left(\neg z\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)\to y=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(K\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)\right)\right)\right)\right\}\right)$$