df-hdmap1 - Mathbox for Norm Megill

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

Definition df-hdmap1 36609

Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 36612 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 36607	. 2 HDMap1
2		vk	. . 3
3		cvv 3113	. . 3
4		vw	. . . 4
5	2	cv 1378	. . . . 5
6		clh 34798	. . . . 5
7	5, 6	cfv 5588	. . . 4
8		va	. . . . . . . . . . . . . 14
9	8	cv 1378	. . . . . . . . . . . . 13
10		vx	. . . . . . . . . . . . . 14
11		vv	. . . . . . . . . . . . . . . . 17
12	11	cv 1378	. . . . . . . . . . . . . . . 16
13		vd	. . . . . . . . . . . . . . . . 17
14	13	cv 1378	. . . . . . . . . . . . . . . 16
15	12, 14	cxp 4997	. . . . . . . . . . . . . . 15
16	15, 12	cxp 4997	. . . . . . . . . . . . . 14
17	10	cv 1378	. . . . . . . . . . . . . . . . 17
18		c2nd 6783	. . . . . . . . . . . . . . . . 17
19	17, 18	cfv 5588	. . . . . . . . . . . . . . . 16
20		vu	. . . . . . . . . . . . . . . . . 18
21	20	cv 1378	. . . . . . . . . . . . . . . . 17
22		c0g 14695	. . . . . . . . . . . . . . . . 17
23	21, 22	cfv 5588	. . . . . . . . . . . . . . . 16
24	19, 23	wceq 1379	. . . . . . . . . . . . . . 15
25		vc	. . . . . . . . . . . . . . . . 17
26	25	cv 1378	. . . . . . . . . . . . . . . 16
27	26, 22	cfv 5588	. . . . . . . . . . . . . . 15
28	19	csn 4027	. . . . . . . . . . . . . . . . . . . 20
29		vn	. . . . . . . . . . . . . . . . . . . . 21
30	29	cv 1378	. . . . . . . . . . . . . . . . . . . 20
31	28, 30	cfv 5588	. . . . . . . . . . . . . . . . . . 19
32		vm	. . . . . . . . . . . . . . . . . . . 20
33	32	cv 1378	. . . . . . . . . . . . . . . . . . 19
34	31, 33	cfv 5588	. . . . . . . . . . . . . . . . . 18
35		vh	. . . . . . . . . . . . . . . . . . . . 21
36	35	cv 1378	. . . . . . . . . . . . . . . . . . . 20
37	36	csn 4027	. . . . . . . . . . . . . . . . . . 19
38		vj	. . . . . . . . . . . . . . . . . . . 20
39	38	cv 1378	. . . . . . . . . . . . . . . . . . 19
40	37, 39	cfv 5588	. . . . . . . . . . . . . . . . . 18
41	34, 40	wceq 1379	. . . . . . . . . . . . . . . . 17
42		c1st 6782	. . . . . . . . . . . . . . . . . . . . . . . 24
43	17, 42	cfv 5588	. . . . . . . . . . . . . . . . . . . . . . 23
44	43, 42	cfv 5588	. . . . . . . . . . . . . . . . . . . . . 22
45		csg 15730	. . . . . . . . . . . . . . . . . . . . . . 23
46	21, 45	cfv 5588	. . . . . . . . . . . . . . . . . . . . . 22
47	44, 19, 46	co 6284	. . . . . . . . . . . . . . . . . . . . 21
48	47	csn 4027	. . . . . . . . . . . . . . . . . . . 20
49	48, 30	cfv 5588	. . . . . . . . . . . . . . . . . . 19
50	49, 33	cfv 5588	. . . . . . . . . . . . . . . . . 18
51	43, 18	cfv 5588	. . . . . . . . . . . . . . . . . . . . 21
52	26, 45	cfv 5588	. . . . . . . . . . . . . . . . . . . . 21
53	51, 36, 52	co 6284	. . . . . . . . . . . . . . . . . . . 20
54	53	csn 4027	. . . . . . . . . . . . . . . . . . 19
55	54, 39	cfv 5588	. . . . . . . . . . . . . . . . . 18
56	50, 55	wceq 1379	. . . . . . . . . . . . . . . . 17
57	41, 56	wa 369	. . . . . . . . . . . . . . . 16 $/\$
58	57, 35, 14	crio 6244	. . . . . . . . . . . . . . 15 $/\$
59	24, 27, 58	cif 3939	. . . . . . . . . . . . . 14 $/\$
60	10, 16, 59	cmpt 4505	. . . . . . . . . . . . 13 $/\$
61	9, 60	wcel 1767	. . . . . . . . . . . 12 $/\$
62	4	cv 1378	. . . . . . . . . . . . 13
63		cmpd 36439	. . . . . . . . . . . . . 14 mapd
64	5, 63	cfv 5588	. . . . . . . . . . . . 13 mapd
65	62, 64	cfv 5588	. . . . . . . . . . . 12 mapd
66	61, 32, 65	wsbc 3331	. . . . . . . . . . 11 mapd $/\$
67		clspn 17417	. . . . . . . . . . . 12
68	26, 67	cfv 5588	. . . . . . . . . . 11
69	66, 38, 68	wsbc 3331	. . . . . . . . . 10 mapd $/\$
70		cbs 14490	. . . . . . . . . . 11
71	26, 70	cfv 5588	. . . . . . . . . 10
72	69, 13, 71	wsbc 3331	. . . . . . . . 9 mapd $/\$
73		clcd 36401	. . . . . . . . . . 11 LCDual
74	5, 73	cfv 5588	. . . . . . . . . 10 LCDual
75	62, 74	cfv 5588	. . . . . . . . 9 LCDual
76	72, 25, 75	wsbc 3331	. . . . . . . 8 LCDual mapd $/\$
77	21, 67	cfv 5588	. . . . . . . 8
78	76, 29, 77	wsbc 3331	. . . . . . 7 LCDual mapd $/\$
79	21, 70	cfv 5588	. . . . . . 7
80	78, 11, 79	wsbc 3331	. . . . . 6 LCDual mapd $/\$
81		cdvh 35893	. . . . . . . 8
82	5, 81	cfv 5588	. . . . . . 7
83	62, 82	cfv 5588	. . . . . 6
84	80, 20, 83	wsbc 3331	. . . . 5 LCDual mapd $/\$
85	84, 8	cab 2452	. . . 4 LCDual mapd $/\$
86	4, 7, 85	cmpt 4505	. . 3 LCDual mapd $/\$
87	2, 3, 86	cmpt 4505	. 2 LCDual mapd $/\$
88	1, 87	wceq 1379	1 HDMap1 LCDual mapd $/\$

Colors of variables: wff setvar class

This definition is referenced by: hdmap1ffval 36611

W3C validator