# Metamath Proof Explorer

## Definition df-hvmap

Description: Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o , dochfl1 - should we update those to use this definition? (Contributed by NM, 23-Mar-2015)

Ref Expression
Assertion df-hvmap ${⊢}\mathrm{HVMap}=\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({x}\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)⟼\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chvm ${class}\mathrm{HVMap}$
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 vx ${setvar}{x}$
8 cbs ${class}\mathrm{Base}$
9 cdvh ${class}\mathrm{DVecH}$
10 5 9 cfv ${class}\mathrm{DVecH}\left({k}\right)$
11 3 cv ${setvar}{w}$
12 11 10 cfv ${class}\mathrm{DVecH}\left({k}\right)\left({w}\right)$
13 12 8 cfv ${class}{\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}$
14 c0g ${class}{0}_{𝑔}$
15 12 14 cfv ${class}{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}$
16 15 csn ${class}\left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}$
17 13 16 cdif ${class}\left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)$
18 vv ${setvar}{v}$
19 vj ${setvar}{j}$
20 csca ${class}\mathrm{Scalar}$
21 12 20 cfv ${class}\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)$
22 21 8 cfv ${class}{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}$
23 vt ${setvar}{t}$
24 coch ${class}\mathrm{ocH}$
25 5 24 cfv ${class}\mathrm{ocH}\left({k}\right)$
26 11 25 cfv ${class}\mathrm{ocH}\left({k}\right)\left({w}\right)$
27 7 cv ${setvar}{x}$
28 27 csn ${class}\left\{{x}\right\}$
29 28 26 cfv ${class}\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)$
30 18 cv ${setvar}{v}$
31 23 cv ${setvar}{t}$
32 cplusg ${class}{+}_{𝑔}$
33 12 32 cfv ${class}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}$
34 19 cv ${setvar}{j}$
35 cvsca ${class}{\cdot }_{𝑠}$
36 12 35 cfv ${class}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}$
37 34 27 36 co ${class}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)$
38 31 37 33 co ${class}\left({t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)$
39 30 38 wceq ${wff}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)$
40 39 23 29 wrex ${wff}\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)$
41 40 19 22 crio ${class}\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)$
42 18 13 41 cmpt ${class}\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)$
43 7 17 42 cmpt ${class}\left({x}\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)⟼\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)\right)$
44 3 6 43 cmpt ${class}\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({x}\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)⟼\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)\right)\right)$
45 1 2 44 cmpt ${class}\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({x}\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)⟼\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)\right)\right)\right)$
46 0 45 wceq ${wff}\mathrm{HVMap}=\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({x}\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}\right)⟼\left({v}\in {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}⟼\left(\iota {j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}|\exists {t}\in \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)\right)\right)\right)\right)\right)$