Theorem hdmap1fval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span J to the convention L for this section. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1val.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1fval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1fval.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1fval.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap1fval.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1fval.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1fval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1fval.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1fval.r	$$⊢R={-}_C$$
	hdmap1fval.q	$$⊢Q=0_C$$
	hdmap1fval.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	hdmap1fval.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1fval.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1fval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
Assertion	hdmap1fval	$$⊢\phi \to I=\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1val.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1fval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1fval.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1fval.s	$$⊢\underset{\dot{}}{-}={-}_U$$
5		hdmap1fval.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap1fval.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		hdmap1fval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap1fval.d	$$⊢D={\mathrm{Base}}_C$$
9		hdmap1fval.r	$$⊢R={-}_C$$
10		hdmap1fval.q	$$⊢Q=0_C$$
11		hdmap1fval.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		hdmap1fval.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
13		hdmap1fval.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
14		hdmap1fval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
15	1	hdmap1ffval	$$⊢K\in A\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)$$
16	15	fveq1d	$$⊢K\in A\to \mathrm{HDMap1}\left(K\right)\left(W\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)\left(W\right)$$
17	13 16	syl5eq	$$⊢K\in A\to I=\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)\left(W\right)$$
18		fveq2	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
19		fveq2	$$⊢w=W\to \mathrm{LCDual}\left(K\right)\left(w\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
20		fveq2	$$⊢w=W\to \mathrm{mapd}\left(K\right)\left(w\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
21	20	sbceq1d	$$⊢w=W\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)$$
22	21	sbcbidv	$$⊢w=W\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)$$
23	22	sbcbidv	$$⊢w=W\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)$$
24	19 23	sbceqbid	$$⊢w=W\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)$$
25	24	sbcbidv	$$⊢w=W\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)$$
26	25	sbcbidv	$$⊢w=W\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)$$
27	18 26	sbceqbid	$$⊢w=W\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)$$
28		fvex	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)\in \mathrm{V}$$
29		fvex	$$⊢{\mathrm{Base}}_u\in \mathrm{V}$$
30		fvex	$$⊢\mathrm{LSpan}\left(u\right)\in \mathrm{V}$$
31	2	eqeq2i	$$⊢u=U\leftrightarrow u=\mathrm{DVecH}\left(K\right)\left(W\right)$$
32	31	biimpri	$$⊢u=\mathrm{DVecH}\left(K\right)\left(W\right)\to u=U$$
33	32	3ad2ant1	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to u=U$$
34		simp2	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to v={\mathrm{Base}}_u$$
35	32	fveq2d	$$⊢u=\mathrm{DVecH}\left(K\right)\left(W\right)\to {\mathrm{Base}}_u={\mathrm{Base}}_U$$
36	35	3ad2ant1	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to {\mathrm{Base}}_u={\mathrm{Base}}_U$$
37	34 36	eqtrd	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to v={\mathrm{Base}}_U$$
38	37 3	eqtr4di	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to v=V$$
39		simp3	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to n=\mathrm{LSpan}\left(u\right)$$
40	33	fveq2d	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to \mathrm{LSpan}\left(u\right)=\mathrm{LSpan}\left(U\right)$$
41	39 40	eqtrd	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to n=\mathrm{LSpan}\left(U\right)$$
42	41 6	eqtr4di	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\to n=N$$
43		fvex	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)\in \mathrm{V}$$
44		fvex	$$⊢{\mathrm{Base}}_c\in \mathrm{V}$$
45		fvex	$$⊢\mathrm{LSpan}\left(c\right)\in \mathrm{V}$$
46		id	$$⊢c=\mathrm{LCDual}\left(K\right)\left(W\right)\to c=\mathrm{LCDual}\left(K\right)\left(W\right)$$
47	46 7	eqtr4di	$$⊢c=\mathrm{LCDual}\left(K\right)\left(W\right)\to c=C$$
48	47	3ad2ant1	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to c=C$$
49		simp2	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to d={\mathrm{Base}}_c$$
50	48	fveq2d	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
51	50 8	eqtr4di	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to {\mathrm{Base}}_c=D$$
52	49 51	eqtrd	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to d=D$$
53		simp3	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to j=\mathrm{LSpan}\left(c\right)$$
54	48	fveq2d	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to \mathrm{LSpan}\left(c\right)=\mathrm{LSpan}\left(C\right)$$
55	54 11	eqtr4di	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to \mathrm{LSpan}\left(c\right)=J$$
56	53 55	eqtrd	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\to j=J$$
57		fvex	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)\in \mathrm{V}$$
58		id	$$⊢m=\mathrm{mapd}\left(K\right)\left(W\right)\to m=\mathrm{mapd}\left(K\right)\left(W\right)$$
59	58 12	eqtr4di	$$⊢m=\mathrm{mapd}\left(K\right)\left(W\right)\to m=M$$
60		fveq1	$$⊢m=M\to m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=M\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)$$
61	60	eqeq1d	$$⊢m=M\to \left(m\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\leftrightarrow M\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\right)$$
62		fveq1	$$⊢m=M\to m\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)=M\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)$$
63	62	eqeq1d	$$⊢m=M\to \left(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)\leftrightarrow 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)$$
64	61 63	anbi12d	$$⊢m=M\to \left(\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)\leftrightarrow \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)$$
65	64	riotabidv	$$⊢m=M\to \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)=\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)$$
66	65	ifeq2d	$$⊢m=M\to 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)=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)$$
67	66	mpteq2dv	$$⊢m=M\to \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)=\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)$$
68	67	eleq2d	$$⊢m=M\to \left(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 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)$$
69	59 68	syl	$$⊢m=\mathrm{mapd}\left(K\right)\left(W\right)\to \left(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 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)$$
70	57 69	sbcie	$$⊢\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 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)$$
71		simp2	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to d=D$$
72		xpeq2	$$⊢d=D\to v\times d=v\times D$$
73	72	xpeq1d	$$⊢d=D\to \left(v\times d\right)\times v=\left(v\times D\right)\times v$$
74	71 73	syl	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left(v\times d\right)\times v=\left(v\times D\right)\times v$$
75		simp1	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to c=C$$
76	75	fveq2d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to 0_c=0_C$$
77	76 10	eqtr4di	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to 0_c=Q$$
78		simp3	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to j=J$$
79	78	fveq1d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to j\left(\left\{h\right\}\right)=J\left(\left\{h\right\}\right)$$
80	79	eqeq2d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left(M\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)\leftrightarrow M\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\right)$$
81	75	fveq2d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to {-}_c={-}_C$$
82	81 9	eqtr4di	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to {-}_c=R$$
83	82	oveqd	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to 2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h=2^{nd}\left(1^{st}\left(x\right)\right)Rh$$
84	83	sneqd	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}=\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}$$
85	78 84	fveq12d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to j\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)$$
86	85	eqeq2d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left(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)\leftrightarrow 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)Rh\right\}\right)\right)$$
87	80 86	anbi12d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left(\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)\leftrightarrow \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)Rh\right\}\right)\right)\right)$$
88	71 87	riotaeqbidv	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \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)=\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)Rh\right\}\right)\right)\right)$$
89	77 88	ifeq12d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to 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)=if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)$$
90	74 89	mpteq12dv	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \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)=\left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)$$
91	90	eleq2d	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\to \left(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 a\in \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)\right)$$
92	70 91	syl5bb	$$⊢\left(c=C\wedge d=D\wedge j=J\right)\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 a\in \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)\right)$$
93	48 52 56 92	syl3anc	$$⊢\left(c=\mathrm{LCDual}\left(K\right)\left(W\right)\wedge d={\mathrm{Base}}_c\wedge j=\mathrm{LSpan}\left(c\right)\right)\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 a\in \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)\right)$$
94	43 44 45 93	sbc3ie	$$⊢\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 a\in \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)$$
95		simp2	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to v=V$$
96	95	xpeq1d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to v\times D=V\times D$$
97	96 95	xpeq12d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(v\times D\right)\times v=\left(V\times D\right)\times V$$
98		simp1	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to u=U$$
99	98	fveq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to 0_u=0_U$$
100	99 5	eqtr4di	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to 0_u=\underset{\dot{}}{0}$$
101	100	eqeq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(2^{nd}\left(x\right)=0_u\leftrightarrow 2^{nd}\left(x\right)=\underset{\dot{}}{0}\right)$$
102		simp3	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to n=N$$
103	102	fveq1d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to n\left(\left\{2^{nd}\left(x\right)\right\}\right)=N\left(\left\{2^{nd}\left(x\right)\right\}\right)$$
104	103	fveqeq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(M\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\leftrightarrow M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\right)$$
105	98	fveq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to {-}_u={-}_U$$
106	105 4	eqtr4di	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to {-}_u=\underset{\dot{}}{-}$$
107	106	oveqd	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to 1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)=1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)$$
108	107	sneqd	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}=\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}$$
109	102 108	fveq12d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)=N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)$$
110	109	fveqeq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(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)Rh\right\}\right)\leftrightarrow M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)$$
111	104 110	anbi12d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(\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)Rh\right\}\right)\right)\leftrightarrow \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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)$$
112	111	riotabidv	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \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)Rh\right\}\right)\right)\right)=\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)$$
113	101 112	ifbieq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)=if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)$$
114	97 113	mpteq12dv	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)=\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
115	114	eleq2d	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\to \left(a\in \left(x\in \left(\left(v\times D\right)\times v\right)⟼if\left(2^{nd}\left(x\right)=0_u,Q,\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)Rh\right\}\right)\right)\right)\right)\right)\leftrightarrow a\in \left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)\right)$$
116	94 115	syl5bb	$$⊢\left(u=U\wedge v=V\wedge n=N\right)\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 a\in \left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)\right)$$
117	33 38 42 116	syl3anc	$$⊢\left(u=\mathrm{DVecH}\left(K\right)\left(W\right)\wedge v={\mathrm{Base}}_u\wedge n=\mathrm{LSpan}\left(u\right)\right)\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 a\in \left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)\right)$$
118	28 29 30 117	sbc3ie	$$⊢\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 a\in \left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
119	27 118	bitrdi	$$⊢w=W\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 a\in \left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)\right)$$
120	119	abbi1dv	$$⊢w=W\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(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
121		eqid	$$⊢\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)=\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)$$
122	3	fvexi	$$⊢V\in \mathrm{V}$$
123	8	fvexi	$$⊢D\in \mathrm{V}$$
124	122 123	xpex	$$⊢V\times D\in \mathrm{V}$$
125	124 122	xpex	$$⊢\left(V\times D\right)\times V\in \mathrm{V}$$
126	125	mptex	$$⊢\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)\in \mathrm{V}$$
127	120 121 126	fvmpt	$$⊢W\in H\to \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)\left(W\right)=\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
128	17 127	sylan9eq	$$⊢\left(K\in A\wedge W\in H\right)\to I=\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
129	14 128	syl	$$⊢\phi \to I=\left(x\in \left(\left(V\times D\right)\times V\right)⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\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)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$