Theorem lcdvbaselfl

Description: A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbasess.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvbasess.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvbasess.v	$$⊢V={\mathrm{Base}}_C$$
	lcdvbasess.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvbasess.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcdvbasess.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvbaselfl.x	$$⊢\phi \to X\in V$$
Assertion	lcdvbaselfl	$$⊢\phi \to X\in F$$

Proof

Step	Hyp	Ref	Expression
1		lcdvbasess.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvbasess.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
3		lcdvbasess.v	$$⊢V={\mathrm{Base}}_C$$
4		lcdvbasess.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		lcdvbasess.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lcdvbasess.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		lcdvbaselfl.x	$$⊢\phi \to X\in V$$
8	1 2 3 4 5 6	lcdvbasess	$$⊢\phi \to V\subseteq F$$
9	8 7	sseldd	$$⊢\phi \to X\in F$$