# Metamath Proof Explorer

## Theorem hvmaplfl

Description: The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses hvmaplfl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmaplfl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmaplfl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmaplfl.z
hvmaplfl.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
hvmaplfl.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmaplfl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hvmaplfl.x
Assertion hvmaplfl ${⊢}{\phi }\to {M}\left({X}\right)\in {F}$

### Proof

Step Hyp Ref Expression
1 hvmaplfl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hvmaplfl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hvmaplfl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hvmaplfl.z
5 hvmaplfl.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
6 hvmaplfl.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
7 hvmaplfl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 hvmaplfl.x
9 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
10 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
11 eqid ${⊢}{0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
12 1 2 3 4 9 10 11 6 7 8 hvmapcl2 ${⊢}{\phi }\to {M}\left({X}\right)\in \left({\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\setminus \left\{{0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\right\}\right)$
13 12 eldifad ${⊢}{\phi }\to {M}\left({X}\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
14 1 9 10 2 5 7 13 lcdvbaselfl ${⊢}{\phi }\to {M}\left({X}\right)\in {F}$