# Metamath Proof Explorer

## Theorem hvmapffval

Description: Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

Ref Expression
Hypothesis hvmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion hvmapffval ${⊢}{K}\in {X}\to \mathrm{HVMap}\left({K}\right)=\left({w}\in {H}⟼\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)$

### Proof

Step Hyp Ref Expression
1 hvmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 elex ${⊢}{K}\in {X}\to {K}\in \mathrm{V}$
3 fveq2 ${⊢}{k}={K}\to \mathrm{LHyp}\left({k}\right)=\mathrm{LHyp}\left({K}\right)$
4 3 1 syl6eqr ${⊢}{k}={K}\to \mathrm{LHyp}\left({k}\right)={H}$
5 fveq2 ${⊢}{k}={K}\to \mathrm{DVecH}\left({k}\right)=\mathrm{DVecH}\left({K}\right)$
6 5 fveq1d ${⊢}{k}={K}\to \mathrm{DVecH}\left({k}\right)\left({w}\right)=\mathrm{DVecH}\left({K}\right)\left({w}\right)$
7 6 fveq2d ${⊢}{k}={K}\to {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}$
8 6 fveq2d ${⊢}{k}={K}\to {0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}={0}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}$
9 8 sneqd ${⊢}{k}={K}\to \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}=\left\{{0}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}\right\}$
10 7 9 difeq12d ${⊢}{k}={K}\to {\mathrm{Base}}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\right\}={\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}\setminus \left\{{0}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}\right\}$
11 6 fveq2d ${⊢}{k}={K}\to \mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)=\mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)$
12 11 fveq2d ${⊢}{k}={K}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)}$
13 fveq2 ${⊢}{k}={K}\to \mathrm{ocH}\left({k}\right)=\mathrm{ocH}\left({K}\right)$
14 13 fveq1d ${⊢}{k}={K}\to \mathrm{ocH}\left({k}\right)\left({w}\right)=\mathrm{ocH}\left({K}\right)\left({w}\right)$
15 14 fveq1d ${⊢}{k}={K}\to \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\left\{{x}\right\}\right)=\mathrm{ocH}\left({K}\right)\left({w}\right)\left(\left\{{x}\right\}\right)$
16 6 fveq2d ${⊢}{k}={K}\to {+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}={+}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}$
17 eqidd ${⊢}{k}={K}\to {t}={t}$
18 6 fveq2d ${⊢}{k}={K}\to {\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}={\cdot }_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}$
19 18 oveqd ${⊢}{k}={K}\to {j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}={j}{\cdot }_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}{x}$
20 16 17 19 oveq123d ${⊢}{k}={K}\to {t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)={t}{+}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}{x}\right)$
21 20 eqeq2d ${⊢}{k}={K}\to \left({v}={t}{+}_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({k}\right)\left({w}\right)}{x}\right)↔{v}={t}{+}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}\left({j}{\cdot }_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}{x}\right)\right)$
22 15 21 rexeqbidv ${⊢}{k}={K}\to \left(\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)↔\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)$
23 12 22 riotaeqbidv ${⊢}{k}={K}\to \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)=\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)$
24 7 23 mpteq12dv ${⊢}{k}={K}\to \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)=\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)$
25 10 24 mpteq12dv ${⊢}{k}={K}\to \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)=\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)$
26 4 25 mpteq12dv ${⊢}{k}={K}\to \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)=\left({w}\in {H}⟼\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)$
27 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)$
28 26 27 1 mptfvmpt ${⊢}{K}\in \mathrm{V}\to \mathrm{HVMap}\left({K}\right)=\left({w}\in {H}⟼\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)$
29 2 28 syl ${⊢}{K}\in {X}\to \mathrm{HVMap}\left({K}\right)=\left({w}\in {H}⟼\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)$