Metamath Proof Explorer

Theorem hvmapcl2

Description: Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses hvmap1o2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmap1o2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmap1o2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmap1o2.z
hvmap1o2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hvmap1o2.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
hvmap1o2.o ${⊢}{O}={0}_{{C}}$
hvmap1o2.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmap1o2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hvmapcl2.x
Assertion hvmapcl2 ${⊢}{\phi }\to {M}\left({X}\right)\in \left({F}\setminus \left\{{O}\right\}\right)$

Proof

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