# Metamath Proof Explorer

## Theorem hvmapfval

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

Ref Expression
Hypotheses hvmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmapval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmapval.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hvmapval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmapval.p
hvmapval.t
hvmapval.z
hvmapval.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
hvmapval.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
hvmapval.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmapval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
Assertion hvmapfval

### Proof

Step Hyp Ref Expression
1 hvmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hvmapval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hvmapval.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
4 hvmapval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 hvmapval.p
6 hvmapval.t
7 hvmapval.z
8 hvmapval.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
9 hvmapval.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
10 hvmapval.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
11 hvmapval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
12 1 hvmapffval ${⊢}{K}\in {A}\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)$
13 12 fveq1d ${⊢}{K}\in {A}\to \mathrm{HVMap}\left({K}\right)\left({W}\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)\left({W}\right)$
14 10 13 syl5eq ${⊢}{K}\in {A}\to {M}=\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)\left({W}\right)$
15 fveq2 ${⊢}{w}={W}\to \mathrm{DVecH}\left({K}\right)\left({w}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
16 15 2 syl6eqr ${⊢}{w}={W}\to \mathrm{DVecH}\left({K}\right)\left({w}\right)={U}$
17 16 fveq2d ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}={\mathrm{Base}}_{{U}}$
18 17 4 syl6eqr ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}={V}$
19 16 fveq2d ${⊢}{w}={W}\to {0}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}={0}_{{U}}$
20 19 7 syl6eqr
21 20 sneqd
22 18 21 difeq12d
23 16 fveq2d ${⊢}{w}={W}\to \mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)=\mathrm{Scalar}\left({U}\right)$
24 23 8 syl6eqr ${⊢}{w}={W}\to \mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)={S}$
25 24 fveq2d ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)}={\mathrm{Base}}_{{S}}$
26 25 9 syl6eqr ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left({K}\right)\left({w}\right)\right)}={R}$
27 fveq2 ${⊢}{w}={W}\to \mathrm{ocH}\left({K}\right)\left({w}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
28 27 3 syl6eqr ${⊢}{w}={W}\to \mathrm{ocH}\left({K}\right)\left({w}\right)={O}$
29 28 fveq1d ${⊢}{w}={W}\to \mathrm{ocH}\left({K}\right)\left({w}\right)\left(\left\{{x}\right\}\right)={O}\left(\left\{{x}\right\}\right)$
30 16 fveq2d ${⊢}{w}={W}\to {+}_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}={+}_{{U}}$
31 30 5 syl6eqr
32 eqidd ${⊢}{w}={W}\to {t}={t}$
33 16 fveq2d ${⊢}{w}={W}\to {\cdot }_{\mathrm{DVecH}\left({K}\right)\left({w}\right)}={\cdot }_{{U}}$
34 33 6 syl6eqr
35 34 oveqd
36 31 32 35 oveq123d
37 36 eqeq2d
38 29 37 rexeqbidv
39 26 38 riotaeqbidv
40 18 39 mpteq12dv
41 22 40 mpteq12dv
42 eqid ${⊢}\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)=\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)$
43 4 fvexi ${⊢}{V}\in \mathrm{V}$
44 43 difexi
45 44 mptex
46 41 42 45 fvmpt
47 14 46 sylan9eq
48 11 47 syl