Theorem hvmapclN

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

	Ref	Expression
Hypotheses	hvmap1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hvmap1o.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hvmap1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmap1o.v	$$⊢V={\mathrm{Base}}_U$$
	hvmap1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmap1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	hvmap1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	hvmap1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	hvmap1o.q	$$⊢Q=0_D$$
	hvmap1o.c	$$⊢C=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	hvmap1o.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmap1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hvmapcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	hvmapclN	$$⊢\phi \to M\left(X\right)\in \left(C\setminus \left\{Q\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvmap1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmap1o.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		hvmap1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		hvmap1o.v	$$⊢V={\mathrm{Base}}_U$$
5		hvmap1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		hvmap1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		hvmap1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		hvmap1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
9		hvmap1o.q	$$⊢Q=0_D$$
10		hvmap1o.c	$$⊢C=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
11		hvmap1o.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
12		hvmap1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		hvmapcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
14	1 2 3 4 5 6 7 8 9 10 11 12	hvmap1o	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$
15		f1of	$$⊢M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}\to M:V\setminus \left\{\underset{\dot{}}{0}\right\}⟶C\setminus \left\{Q\right\}$$
16	14 15	syl	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}⟶C\setminus \left\{Q\right\}$$
17	16 13	ffvelrnd	$$⊢\phi \to M\left(X\right)\in \left(C\setminus \left\{Q\right\}\right)$$