Definition df-hdmap

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chdma	$$class\mathrm{HDMap}$$
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		cid	$$class\mathrm{I}$$
9		cbs	$$class\mathrm{Base}$$
10	5 9	cfv	$$class{\mathrm{Base}}_k$$
11	8 10	cres	$$class\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k}\right)$$
12		cltrn	$$class\mathrm{LTrn}$$
13	5 12	cfv	$$class\mathrm{LTrn}\left(k\right)$$
14	3	cv	$$setvarw$$
15	14 13	cfv	$$class\mathrm{LTrn}\left(k\right)\left(w\right)$$
16	8 15	cres	$$class\left({\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}\right)$$
17	11 16	cop	$$class⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_k},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(k\right)\left(w\right)}⟩$$
18		ve	$$setvare$$
19		cdvh	$$class\mathrm{DVecH}$$
20	5 19	cfv	$$class\mathrm{DVecH}\left(k\right)$$
21	14 20	cfv	$$class\mathrm{DVecH}\left(k\right)\left(w\right)$$
22		vu	$$setvaru$$
23	22	cv	$$setvaru$$
24	23 9	cfv	$$class{\mathrm{Base}}_u$$
25		vv	$$setvarv$$
26		chdma1	$$class\mathrm{HDMap1}$$
27	5 26	cfv	$$class\mathrm{HDMap1}\left(k\right)$$
28	14 27	cfv	$$class\mathrm{HDMap1}\left(k\right)\left(w\right)$$
29		vi	$$setvari$$
30	7	cv	$$setvara$$
31		vt	$$setvart$$
32	25	cv	$$setvarv$$
33		vy	$$setvary$$
34		clcd	$$class\mathrm{LCDual}$$
35	5 34	cfv	$$class\mathrm{LCDual}\left(k\right)$$
36	14 35	cfv	$$class\mathrm{LCDual}\left(k\right)\left(w\right)$$
37	36 9	cfv	$$class{\mathrm{Base}}_{\mathrm{LCDual}\left(k\right)\left(w\right)}$$
38		vz	$$setvarz$$
39	38	cv	$$setvarz$$
40		clspn	$$class\mathrm{LSpan}$$
41	23 40	cfv	$$class\mathrm{LSpan}\left(u\right)$$
42	18	cv	$$setvare$$
43	42	csn	$$class\left\{e\right\}$$
44	43 41	cfv	$$class\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)$$
45	31	cv	$$setvart$$
46	45	csn	$$class\left\{t\right\}$$
47	46 41	cfv	$$class\mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)$$
48	44 47	cun	$$class\left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)$$
49	39 48	wcel	$$wffz\in \left(\mathrm{LSpan}\left(u\right)\left(\left\{e\right\}\right)\cup \mathrm{LSpan}\left(u\right)\left(\left\{t\right\}\right)\right)$$
50	49	wn	$$wff\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)$$
51	33	cv	$$setvary$$
52	29	cv	$$setvari$$
53		chvm	$$class\mathrm{HVMap}$$
54	5 53	cfv	$$class\mathrm{HVMap}\left(k\right)$$
55	14 54	cfv	$$class\mathrm{HVMap}\left(k\right)\left(w\right)$$
56	42 55	cfv	$$class\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right)$$
57	42 56 39	cotp	$$class⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩$$
58	57 52	cfv	$$classi\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right)$$
59	39 58 45	cotp	$$class⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩$$
60	59 52	cfv	$$classi\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)$$
61	51 60	wceq	$$wffy=i\left(⟨z,i\left(⟨e,\mathrm{HVMap}\left(k\right)\left(w\right)\left(e\right),z⟩\right),t⟩\right)$$
62	50 61	wi	$$wff\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)$$
63	62 38 32	wral	$$wff\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)$$
64	63 33 37	crio	$$class\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)$$
65	31 32 64	cmpt	$$class\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)$$
66	30 65	wcel	$$wffa\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)$$
67	66 29 28	wsbc	$$wff\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)$$
68	67 25 24	wsbc	$$wff\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)$$
69	68 22 21	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{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)$$
70	69 18 17	wsbc	$$wff\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)$$
71	70 7	cab	$$class\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\}$$
72	3 6 71	cmpt	$$class\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)$$
73	1 2 72	cmpt	$$class\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)$$
74	0 73	wceq	$$wff\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)$$