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 = ( LHyp ` K )
	lcdvbasess.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvbasess.v	|- V = ( Base ` C )
	lcdvbasess.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvbasess.f	|- F = ( LFnl ` U )
	lcdvbasess.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdvbaselfl.x	|- ( ph -> X e. V )
Assertion	lcdvbaselfl	|- ( ph -> X e. F )

Proof

Step	Hyp	Ref	Expression
1		lcdvbasess.h	|- H = ( LHyp ` K )
2		lcdvbasess.c	|- C = ( ( LCDual ` K ) ` W )
3		lcdvbasess.v	|- V = ( Base ` C )
4		lcdvbasess.u	|- U = ( ( DVecH ` K ) ` W )
5		lcdvbasess.f	|- F = ( LFnl ` U )
6		lcdvbasess.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		lcdvbaselfl.x	|- ( ph -> X e. V )
8	1 2 3 4 5 6	lcdvbasess	|- ( ph -> V C_ F )
9	8 7	sseldd	|- ( ph -> X e. F )