df-hdmap1 - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-hdmap1		Unicode version

Definition df-hdmap1 32277

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

**Assertion**
Ref	Expression
df-hdmap1	HDMap1 LCDual mapd $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-hdmap1**
Step	Hyp	Ref	Expression
1		chdma1 32275	. 2 HDMap1
2		vk	. . 3
3		cvv 2916	. . 3
4		vw	. . . 4
5	2	cv 1648	. . . . 5
6		clh 30466	. . . . 5
7	5, 6	cfv 5413	. . . 4
8		va	. . . . . . . . . . . . . 14
9	8	cv 1648	. . . . . . . . . . . . 13
10		vx	. . . . . . . . . . . . . 14
11		vv	. . . . . . . . . . . . . . . . 17
12	11	cv 1648	. . . . . . . . . . . . . . . 16
13		vd	. . . . . . . . . . . . . . . . 17
14	13	cv 1648	. . . . . . . . . . . . . . . 16
15	12, 14	cxp 4835	. . . . . . . . . . . . . . 15
16	15, 12	cxp 4835	. . . . . . . . . . . . . 14
17	10	cv 1648	. . . . . . . . . . . . . . . . 17
18		c2nd 6307	. . . . . . . . . . . . . . . . 17
19	17, 18	cfv 5413	. . . . . . . . . . . . . . . 16
20		vu	. . . . . . . . . . . . . . . . . 18
21	20	cv 1648	. . . . . . . . . . . . . . . . 17
22		c0g 13678	. . . . . . . . . . . . . . . . 17
23	21, 22	cfv 5413	. . . . . . . . . . . . . . . 16
24	19, 23	wceq 1649	. . . . . . . . . . . . . . 15
25		vc	. . . . . . . . . . . . . . . . 17
26	25	cv 1648	. . . . . . . . . . . . . . . 16
27	26, 22	cfv 5413	. . . . . . . . . . . . . . 15
28	19	csn 3774	. . . . . . . . . . . . . . . . . . . 20
29		vn	. . . . . . . . . . . . . . . . . . . . 21
30	29	cv 1648	. . . . . . . . . . . . . . . . . . . 20
31	28, 30	cfv 5413	. . . . . . . . . . . . . . . . . . 19
32		vm	. . . . . . . . . . . . . . . . . . . 20
33	32	cv 1648	. . . . . . . . . . . . . . . . . . 19
34	31, 33	cfv 5413	. . . . . . . . . . . . . . . . . 18
35		vh	. . . . . . . . . . . . . . . . . . . . 21
36	35	cv 1648	. . . . . . . . . . . . . . . . . . . 20
37	36	csn 3774	. . . . . . . . . . . . . . . . . . 19
38		vj	. . . . . . . . . . . . . . . . . . . 20
39	38	cv 1648	. . . . . . . . . . . . . . . . . . 19
40	37, 39	cfv 5413	. . . . . . . . . . . . . . . . . 18
41	34, 40	wceq 1649	. . . . . . . . . . . . . . . . 17
42		c1st 6306	. . . . . . . . . . . . . . . . . . . . . . . 24
43	17, 42	cfv 5413	. . . . . . . . . . . . . . . . . . . . . . 23
44	43, 42	cfv 5413	. . . . . . . . . . . . . . . . . . . . . 22
45		csg 14643	. . . . . . . . . . . . . . . . . . . . . . 23
46	21, 45	cfv 5413	. . . . . . . . . . . . . . . . . . . . . 22
47	44, 19, 46	co 6040	. . . . . . . . . . . . . . . . . . . . 21
48	47	csn 3774	. . . . . . . . . . . . . . . . . . . 20
49	48, 30	cfv 5413	. . . . . . . . . . . . . . . . . . 19
50	49, 33	cfv 5413	. . . . . . . . . . . . . . . . . 18
51	43, 18	cfv 5413	. . . . . . . . . . . . . . . . . . . . 21
52	26, 45	cfv 5413	. . . . . . . . . . . . . . . . . . . . 21
53	51, 36, 52	co 6040	. . . . . . . . . . . . . . . . . . . 20
54	53	csn 3774	. . . . . . . . . . . . . . . . . . 19
55	54, 39	cfv 5413	. . . . . . . . . . . . . . . . . 18
56	50, 55	wceq 1649	. . . . . . . . . . . . . . . . 17
57	41, 56	wa 359	. . . . . . . . . . . . . . . 16 $/\$
58	57, 35, 14	crio 6501	. . . . . . . . . . . . . . 15 $/\$
59	24, 27, 58	cif 3699	. . . . . . . . . . . . . 14 $/\$
60	10, 16, 59	cmpt 4226	. . . . . . . . . . . . 13 $/\$
61	9, 60	wcel 1721	. . . . . . . . . . . 12 $/\$
62	4	cv 1648	. . . . . . . . . . . . 13
63		cmpd 32107	. . . . . . . . . . . . . 14 mapd
64	5, 63	cfv 5413	. . . . . . . . . . . . 13 mapd
65	62, 64	cfv 5413	. . . . . . . . . . . 12 mapd
66	61, 32, 65	wsbc 3121	. . . . . . . . . . 11 mapd $/\$
67		clspn 16002	. . . . . . . . . . . 12
68	26, 67	cfv 5413	. . . . . . . . . . 11
69	66, 38, 68	wsbc 3121	. . . . . . . . . 10 mapd $/\$
70		cbs 13424	. . . . . . . . . . 11
71	26, 70	cfv 5413	. . . . . . . . . 10
72	69, 13, 71	wsbc 3121	. . . . . . . . 9 mapd $/\$
73		clcd 32069	. . . . . . . . . . 11 LCDual
74	5, 73	cfv 5413	. . . . . . . . . 10 LCDual
75	62, 74	cfv 5413	. . . . . . . . 9 LCDual
76	72, 25, 75	wsbc 3121	. . . . . . . 8 LCDual mapd $/\$
77	21, 67	cfv 5413	. . . . . . . 8
78	76, 29, 77	wsbc 3121	. . . . . . 7 LCDual mapd $/\$
79	21, 70	cfv 5413	. . . . . . 7
80	78, 11, 79	wsbc 3121	. . . . . 6 LCDual mapd $/\$
81		cdvh 31561	. . . . . . . 8
82	5, 81	cfv 5413	. . . . . . 7
83	62, 82	cfv 5413	. . . . . 6
84	80, 20, 83	wsbc 3121	. . . . 5 LCDual mapd $/\$
85	84, 8	cab 2390	. . . 4 LCDual mapd $/\$
86	4, 7, 85	cmpt 4226	. . 3 LCDual mapd $/\$
87	2, 3, 86	cmpt 4226	. 2 LCDual mapd $/\$
88	1, 87	wceq 1649	1 HDMap1 LCDual mapd $/\$

Colors of variables: wff set class

This definition is referenced by: hdmap1ffval 32279

W3C validator