# Metamath Proof Explorer

## Theorem hgmapdcl

Description: Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hgmapdcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hgmapdcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hgmapdcl.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hgmapdcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hgmapdcl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hgmapdcl.q ${⊢}{Q}=\mathrm{Scalar}\left({C}\right)$
hgmapdcl.a ${⊢}{A}={\mathrm{Base}}_{{Q}}$
hgmapdcl.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hgmapdcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hgmapdcl.f ${⊢}{\phi }\to {F}\in {B}$
Assertion hgmapdcl ${⊢}{\phi }\to {G}\left({F}\right)\in {A}$

### Proof

Step Hyp Ref Expression
1 hgmapdcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hgmapdcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hgmapdcl.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
4 hgmapdcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
5 hgmapdcl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 hgmapdcl.q ${⊢}{Q}=\mathrm{Scalar}\left({C}\right)$
7 hgmapdcl.a ${⊢}{A}={\mathrm{Base}}_{{Q}}$
8 hgmapdcl.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
9 hgmapdcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 hgmapdcl.f ${⊢}{\phi }\to {F}\in {B}$
11 1 2 3 4 8 9 10 hgmapcl ${⊢}{\phi }\to {G}\left({F}\right)\in {B}$
12 1 2 3 4 5 6 7 9 lcdsbase ${⊢}{\phi }\to {A}={B}$
13 11 12 eleqtrrd ${⊢}{\phi }\to {G}\left({F}\right)\in {A}$