# Metamath Proof Explorer

## Theorem hvmap1o

Description: The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses hvmap1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmap1o.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hvmap1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmap1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmap1o.z
hvmap1o.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
hvmap1o.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
hvmap1o.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
hvmap1o.q ${⊢}{Q}={0}_{{D}}$
hvmap1o.c ${⊢}{C}=\left\{{f}\in {F}|{O}\left({O}\left({L}\left({f}\right)\right)\right)={L}\left({f}\right)\right\}$
hvmap1o.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmap1o.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hvmap1o

### Proof

Step Hyp Ref Expression
1 hvmap1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hvmap1o.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
3 hvmap1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 hvmap1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 hvmap1o.z
6 hvmap1o.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
7 hvmap1o.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
8 hvmap1o.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
9 hvmap1o.q ${⊢}{Q}={0}_{{D}}$
10 hvmap1o.c ${⊢}{C}=\left\{{f}\in {F}|{O}\left({O}\left({L}\left({f}\right)\right)\right)={L}\left({f}\right)\right\}$
11 hvmap1o.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
12 hvmap1o.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
13 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
14 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
15 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
16 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}$
17 eqid
18 1 2 3 4 13 14 15 16 5 6 7 8 9 10 17 12 lcf1o
19 1 3 2 4 13 14 5 15 16 11 12 hvmapfval
20 f1oeq1
21 19 20 syl
22 18 21 mpbird