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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | chdma1 | |
|
1 | vk | |
|
2 | cvv | |
|
3 | vw | |
|
4 | clh | |
|
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | va | |
|
8 | cdvh | |
|
9 | 5 8 | cfv | |
10 | 3 | cv | |
11 | 10 9 | cfv | |
12 | vu | |
|
13 | cbs | |
|
14 | 12 | cv | |
15 | 14 13 | cfv | |
16 | vv | |
|
17 | clspn | |
|
18 | 14 17 | cfv | |
19 | vn | |
|
20 | clcd | |
|
21 | 5 20 | cfv | |
22 | 10 21 | cfv | |
23 | vc | |
|
24 | 23 | cv | |
25 | 24 13 | cfv | |
26 | vd | |
|
27 | 24 17 | cfv | |
28 | vj | |
|
29 | cmpd | |
|
30 | 5 29 | cfv | |
31 | 10 30 | cfv | |
32 | vm | |
|
33 | 7 | cv | |
34 | vx | |
|
35 | 16 | cv | |
36 | 26 | cv | |
37 | 35 36 | cxp | |
38 | 37 35 | cxp | |
39 | c2nd | |
|
40 | 34 | cv | |
41 | 40 39 | cfv | |
42 | c0g | |
|
43 | 14 42 | cfv | |
44 | 41 43 | wceq | |
45 | 24 42 | cfv | |
46 | vh | |
|
47 | 32 | cv | |
48 | 19 | cv | |
49 | 41 | csn | |
50 | 49 48 | cfv | |
51 | 50 47 | cfv | |
52 | 28 | cv | |
53 | 46 | cv | |
54 | 53 | csn | |
55 | 54 52 | cfv | |
56 | 51 55 | wceq | |
57 | c1st | |
|
58 | 40 57 | cfv | |
59 | 58 57 | cfv | |
60 | csg | |
|
61 | 14 60 | cfv | |
62 | 59 41 61 | co | |
63 | 62 | csn | |
64 | 63 48 | cfv | |
65 | 64 47 | cfv | |
66 | 58 39 | cfv | |
67 | 24 60 | cfv | |
68 | 66 53 67 | co | |
69 | 68 | csn | |
70 | 69 52 | cfv | |
71 | 65 70 | wceq | |
72 | 56 71 | wa | |
73 | 72 46 36 | crio | |
74 | 44 45 73 | cif | |
75 | 34 38 74 | cmpt | |
76 | 33 75 | wcel | |
77 | 76 32 31 | wsbc | |
78 | 77 28 27 | wsbc | |
79 | 78 26 25 | wsbc | |
80 | 79 23 22 | wsbc | |
81 | 80 19 18 | wsbc | |
82 | 81 16 15 | wsbc | |
83 | 82 12 11 | wsbc | |
84 | 83 7 | cab | |
85 | 3 6 84 | cmpt | |
86 | 1 2 85 | cmpt | |
87 | 0 86 | wceq | |