# Metamath Proof Explorer

## 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chdma1 ${class}\mathrm{HDMap1}$
1 vk ${setvar}{k}$
2 cvv ${class}\mathrm{V}$
3 vw ${setvar}{w}$
4 clh ${class}\mathrm{LHyp}$
5 1 cv ${setvar}{k}$
6 5 4 cfv ${class}\mathrm{LHyp}\left({k}\right)$
7 va ${setvar}{a}$
8 cdvh ${class}\mathrm{DVecH}$
9 5 8 cfv ${class}\mathrm{DVecH}\left({k}\right)$
10 3 cv ${setvar}{w}$
11 10 9 cfv ${class}\mathrm{DVecH}\left({k}\right)\left({w}\right)$
12 vu ${setvar}{u}$
13 cbs ${class}\mathrm{Base}$
14 12 cv ${setvar}{u}$
15 14 13 cfv ${class}{\mathrm{Base}}_{{u}}$
16 vv ${setvar}{v}$
17 clspn ${class}\mathrm{LSpan}$
18 14 17 cfv ${class}\mathrm{LSpan}\left({u}\right)$
19 vn ${setvar}{n}$
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 ${setvar}{c}$
24 23 cv ${setvar}{c}$
25 24 13 cfv ${class}{\mathrm{Base}}_{{c}}$
26 vd ${setvar}{d}$
27 24 17 cfv ${class}\mathrm{LSpan}\left({c}\right)$
28 vj ${setvar}{j}$
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 ${setvar}{m}$
33 7 cv ${setvar}{a}$
34 vx ${setvar}{x}$
35 16 cv ${setvar}{v}$
36 26 cv ${setvar}{d}$
37 35 36 cxp ${class}\left({v}×{d}\right)$
38 37 35 cxp ${class}\left(\left({v}×{d}\right)×{v}\right)$
39 c2nd ${class}{2}^{nd}$
40 34 cv ${setvar}{x}$
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 ${setvar}{h}$
47 32 cv ${setvar}{m}$
48 19 cv ${setvar}{n}$
49 41 csn ${class}\left\{{2}^{nd}\left({x}\right)\right\}$
50 49 48 cfv ${class}{n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)$
51 50 47 cfv ${class}{m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)$
52 28 cv ${setvar}{j}$
53 46 cv ${setvar}{h}$
54 53 csn ${class}\left\{{h}\right\}$
55 54 52 cfv ${class}{j}\left(\left\{{h}\right\}\right)$
56 51 55 wceq ${wff}{m}\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 ${class}{n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)$
65 64 47 cfv ${class}{m}\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 ${class}{j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)$
71 65 70 wceq ${wff}{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)$
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 ${class}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)$
75 34 38 74 cmpt ${class}\left({x}\in \left(\left({v}×{d}\right)×{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 ${wff}{a}\in \left({x}\in \left(\left({v}×{d}\right)×{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
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