Theorem hvmaplfl

Description: The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	hvmaplfl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hvmaplfl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmaplfl.v	$$⊢V={\mathrm{Base}}_U$$
	hvmaplfl.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmaplfl.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	hvmaplfl.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmaplfl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hvmaplfl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	hvmaplfl	$$⊢\phi \to M\left(X\right)\in F$$

Proof

Step	Hyp	Ref	Expression
1		hvmaplfl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmaplfl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hvmaplfl.v	$$⊢V={\mathrm{Base}}_U$$
4		hvmaplfl.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		hvmaplfl.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		hvmaplfl.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
7		hvmaplfl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		hvmaplfl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
11		eqid	$$⊢0_{\mathrm{LCDual}\left(K\right)\left(W\right)}=0_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
12	1 2 3 4 9 10 11 6 7 8	hvmapcl2	$$⊢\phi \to M\left(X\right)\in \left({\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}\setminus \left\{0_{\mathrm{LCDual}\left(K\right)\left(W\right)}\right\}\right)$$
13	12	eldifad	$$⊢\phi \to M\left(X\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
14	1 9 10 2 5 7 13	lcdvbaselfl	$$⊢\phi \to M\left(X\right)\in F$$