# Metamath Proof Explorer

## Theorem hdmap1val0

Description: Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 .) (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmap1val0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1val0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1val0.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1val0.o
hdmap1val0.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1val0.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1val0.q ${⊢}{Q}={0}_{{C}}$
hdmap1val0.s ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1val0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmap1val0.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1val0.x ${⊢}{\phi }\to {X}\in {V}$
Assertion hdmap1val0

### Proof

Step Hyp Ref Expression
1 hdmap1val0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1val0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1val0.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1val0.o
5 hdmap1val0.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 hdmap1val0.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
7 hdmap1val0.q ${⊢}{Q}={0}_{{C}}$
8 hdmap1val0.s ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
9 hdmap1val0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 hdmap1val0.f ${⊢}{\phi }\to {F}\in {D}$
11 hdmap1val0.x ${⊢}{\phi }\to {X}\in {V}$
12 eqid ${⊢}{-}_{{U}}={-}_{{U}}$
13 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
14 eqid ${⊢}{-}_{{C}}={-}_{{C}}$
15 eqid ${⊢}\mathrm{LSpan}\left({C}\right)=\mathrm{LSpan}\left({C}\right)$
16 eqid ${⊢}\mathrm{mapd}\left({K}\right)\left({W}\right)=\mathrm{mapd}\left({K}\right)\left({W}\right)$
17 1 2 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
18 3 4 lmod0vcl
19 17 18 syl
20 1 2 3 12 4 13 5 6 14 7 15 16 8 9 11 10 19 hdmap1val
21 eqid
22 21 iftruei
23 20 22 eqtrdi