Theorem lcdvbasecl

Description: Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbasecl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvbasecl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvbasecl.v	$$⊢V={\mathrm{Base}}_U$$
	lcdvbasecl.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcdvbasecl.r	$$⊢R={\mathrm{Base}}_S$$
	lcdvbasecl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvbasecl.e	$$⊢E={\mathrm{Base}}_C$$
	lcdvbasecl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvbasecl.f	$$⊢\phi \to F\in E$$
	lcdvbasecl.x	$$⊢\phi \to X\in V$$
Assertion	lcdvbasecl	$$⊢\phi \to F\left(X\right)\in R$$

Proof

Step	Hyp	Ref	Expression
1		lcdvbasecl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvbasecl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvbasecl.v	$$⊢V={\mathrm{Base}}_U$$
4		lcdvbasecl.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
5		lcdvbasecl.r	$$⊢R={\mathrm{Base}}_S$$
6		lcdvbasecl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		lcdvbasecl.e	$$⊢E={\mathrm{Base}}_C$$
8		lcdvbasecl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		lcdvbasecl.f	$$⊢\phi \to F\in E$$
10		lcdvbasecl.x	$$⊢\phi \to X\in V$$
11	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
12		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
13	1 6 7 2 12 8 9	lcdvbaselfl	$$⊢\phi \to F\in \mathrm{LFnl}\left(U\right)$$
14	4 5 3 12	lflcl	$$⊢\left(U\in \mathrm{LMod}\wedge F\in \mathrm{LFnl}\left(U\right)\wedge X\in V\right)\to F\left(X\right)\in R$$
15	11 13 10 14	syl3anc	$$⊢\phi \to F\left(X\right)\in R$$