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	$$⊢\underset{\dot{}}{0}=0_U$$
	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	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
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	$$⊢\underset{\dot{}}{0}=0_U$$
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	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11	1 2 3 4 5 6 7 8 9	hvmap1o2	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}$$
12		f1of	$$⊢M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}\to M:V\setminus \left\{\underset{\dot{}}{0}\right\}⟶F\setminus \left\{O\right\}$$
13	11 12	syl	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}⟶F\setminus \left\{O\right\}$$
14	13 10	ffvelrnd	$$⊢\phi \to M\left(X\right)\in \left(F\setminus \left\{O\right\}\right)$$