Theorem hdmap1ffval

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

	Ref	Expression
Hypothesis	hdmap1val.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	hdmap1ffval	$$⊢K\in X\to \mathrm{HDMap1}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1val.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{DVecH}\left(k\right)=\mathrm{DVecH}\left(K\right)$$
6	5	fveq1d	$$⊢k=K\to \mathrm{DVecH}\left(k\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(w\right)$$
7		fveq2	$$⊢k=K\to \mathrm{LCDual}\left(k\right)=\mathrm{LCDual}\left(K\right)$$
8	7	fveq1d	$$⊢k=K\to \mathrm{LCDual}\left(k\right)\left(w\right)=\mathrm{LCDual}\left(K\right)\left(w\right)$$
9		fveq2	$$⊢k=K\to \mathrm{mapd}\left(k\right)=\mathrm{mapd}\left(K\right)$$
10	9	fveq1d	$$⊢k=K\to \mathrm{mapd}\left(k\right)\left(w\right)=\mathrm{mapd}\left(K\right)\left(w\right)$$
11	10	sbceq1d	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
12	11	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
13	12	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
14	8 13	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
15	14	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
16	15	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
17	6 16	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{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\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{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right)$$
18	17	abbidv	$$⊢k=K\to \left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}=\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}$$
19	4 18	mpteq12dv	$$⊢k=K\to \left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)$$
20		df-hdmap1	$$⊢\mathrm{HDMap1}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(k\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)\right)$$
21	19 20 1	mptfvmpt	$$⊢K\in \mathrm{V}\to \mathrm{HDMap1}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)$$
22	2 21	syl	$$⊢K\in X\to \mathrm{HDMap1}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_u/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(u\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LCDual}\left(K\right)\left(w\right)/c\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_c/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{LSpan}\left(c\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mapd}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in \left(\left(v\times d\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,0_c,\left(\iota h\in d|\left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\wedge m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)\right)\right)\right)\right)\right\}\right)$$