Definition df-hdmap1

Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval description for more details. (Contributed by NM, 14-May-2015)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chdma1	$$class\mathrm{HDMap1}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		va	$$setvara$$
8		cdvh	$$class\mathrm{DVecH}$$
9	5 8	cfv	$$class\mathrm{DVecH}\left(k\right)$$
10	3	cv	$$setvarw$$
11	10 9	cfv	$$class\mathrm{DVecH}\left(k\right)\left(w\right)$$
12		vu	$$setvaru$$
13		cbs	$$class\mathrm{Base}$$
14	12	cv	$$setvaru$$
15	14 13	cfv	$$class{\mathrm{Base}}_u$$
16		vv	$$setvarv$$
17		clspn	$$class\mathrm{LSpan}$$
18	14 17	cfv	$$class\mathrm{LSpan}\left(u\right)$$
19		vn	$$setvarn$$
20		clcd	$$class\mathrm{LCDual}$$
21	5 20	cfv	$$class\mathrm{LCDual}\left(k\right)$$
22	10 21	cfv	$$class\mathrm{LCDual}\left(k\right)\left(w\right)$$
23		vc	$$setvarc$$
24	23	cv	$$setvarc$$
25	24 13	cfv	$$class{\mathrm{Base}}_c$$
26		vd	$$setvard$$
27	24 17	cfv	$$class\mathrm{LSpan}\left(c\right)$$
28		vj	$$setvarj$$
29		cmpd	$$class\mathrm{mapd}$$
30	5 29	cfv	$$class\mathrm{mapd}\left(k\right)$$
31	10 30	cfv	$$class\mathrm{mapd}\left(k\right)\left(w\right)$$
32		vm	$$setvarm$$
33	7	cv	$$setvara$$
34		vx	$$setvarx$$
35	16	cv	$$setvarv$$
36	26	cv	$$setvard$$
37	35 36	cxp	$$class\left(v\times d\right)$$
38	37 35	cxp	$$class\left(\left(v\times d\right)\times v\right)$$
39		c2nd	$$class{2}^{nd}$$
40	34	cv	$$setvarx$$
41	40 39	cfv	$$class{2}^{nd}\left(x\right)$$
42		c0g	$$class{0}_{𝑔}$$
43	14 42	cfv	$$class{0}_u$$
44	41 43	wceq	$$wff{2}^{nd}\left(x\right)=0_u$$
45	24 42	cfv	$$class{0}_c$$
46		vh	$$setvarh$$
47	32	cv	$$setvarm$$
48	19	cv	$$setvarn$$
49	41	csn	$$class\left\{2^{nd}\left(x\right)\right\}$$
50	49 48	cfv	$$classn\left(\left\{2^{nd}\left(x\right)\right\}\right)$$
51	50 47	cfv	$$classm\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)$$
52	28	cv	$$setvarj$$
53	46	cv	$$setvarh$$
54	53	csn	$$class\left\{h\right\}$$
55	54 52	cfv	$$classj\left(\left\{h\right\}\right)$$
56	51 55	wceq	$$wffm\left(n\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=j\left(\left\{h\right\}\right)$$
57		c1st	$$class{1}^{st}$$
58	40 57	cfv	$$class{1}^{st}\left(x\right)$$
59	58 57	cfv	$$class{1}^{st}\left(1^{st}\left(x\right)\right)$$
60		csg	$$class{-}_{𝑔}$$
61	14 60	cfv	$$class{-}_u$$
62	59 41 61	co	$$class\left(1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right)$$
63	62	csn	$$class\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}$$
64	63 48	cfv	$$classn\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)$$
65	64 47	cfv	$$classm\left(n\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_u{2}^{nd}\left(x\right)\right\}\right)\right)$$
66	58 39	cfv	$$class{2}^{nd}\left(1^{st}\left(x\right)\right)$$
67	24 60	cfv	$$class{-}_c$$
68	66 53 67	co	$$class\left(2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right)$$
69	68	csn	$$class\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}$$
70	69 52	cfv	$$classj\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{c}h\right\}\right)$$
71	65 70	wceq	$$wffm\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)$$
72	56 71	wa	$$wff\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)$$
73	72 46 36	crio	$$class\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)$$
74	44 45 73	cif	$$classif\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)$$
75	34 38 74	cmpt	$$class\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)$$
76	33 75	wcel	$$wffa\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)$$
77	76 32 31	wsbc	$$wff\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)$$
78	77 28 27	wsbc	$$wff\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)$$
79	78 26 25	wsbc	$$wff\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)$$
80	79 23 22	wsbc	$$wff\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)$$
81	80 19 18	wsbc	$$wff\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)$$
82	81 16 15	wsbc	$$wff\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)$$
83	82 12 11	wsbc	$$wff\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)$$
84	83 7	cab	$$class\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\}$$
85	3 6 84	cmpt	$$class\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)$$
86	1 2 85	cmpt	$$class\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)$$
87	0 86	wceq	$$wff\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)$$