# Metamath Proof Explorer

## Theorem hdmap1ffval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015)

Ref Expression
Hypothesis hdmap1val.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion hdmap1ffval

### Proof

Step Hyp Ref Expression
1 hdmap1val.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 fveq2 ${⊢}{k}={K}\to \mathrm{LCDual}\left({k}\right)=\mathrm{LCDual}\left({K}\right)$
8 7 fveq1d ${⊢}{k}={K}\to \mathrm{LCDual}\left({k}\right)\left({w}\right)=\mathrm{LCDual}\left({K}\right)\left({w}\right)$
9 fveq2 ${⊢}{k}={K}\to \mathrm{mapd}\left({k}\right)=\mathrm{mapd}\left({K}\right)$
10 9 fveq1d ${⊢}{k}={K}\to \mathrm{mapd}\left({k}\right)\left({w}\right)=\mathrm{mapd}\left({K}\right)\left({w}\right)$
11 10 sbceq1d
12 11 sbcbidv
13 12 sbcbidv
14 8 13 sbceqbid
15 14 sbcbidv
16 15 sbcbidv
17 6 16 sbceqbid
18 17 abbidv
19 4 18 mpteq12dv
20 df-hdmap1
21 19 20 1 mptfvmpt
22 2 21 syl