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 = ( LHyp ` K )
	lcdvbasecl.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvbasecl.v	|- V = ( Base ` U )
	lcdvbasecl.s	|- S = ( Scalar ` U )
	lcdvbasecl.r	|- R = ( Base ` S )
	lcdvbasecl.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvbasecl.e	|- E = ( Base ` C )
	lcdvbasecl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdvbasecl.f	|- ( ph -> F e. E )
	lcdvbasecl.x	|- ( ph -> X e. V )
Assertion	lcdvbasecl	|- ( ph -> ( F ` X ) e. R )

Proof

Step	Hyp	Ref	Expression
1		lcdvbasecl.h	|- H = ( LHyp ` K )
2		lcdvbasecl.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdvbasecl.v	|- V = ( Base ` U )
4		lcdvbasecl.s	|- S = ( Scalar ` U )
5		lcdvbasecl.r	|- R = ( Base ` S )
6		lcdvbasecl.c	|- C = ( ( LCDual ` K ) ` W )
7		lcdvbasecl.e	|- E = ( Base ` C )
8		lcdvbasecl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		lcdvbasecl.f	|- ( ph -> F e. E )
10		lcdvbasecl.x	|- ( ph -> X e. V )
11	1 2 8	dvhlmod	|- ( ph -> U e. LMod )
12		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
13	1 6 7 2 12 8 9	lcdvbaselfl	|- ( ph -> F e. ( LFnl ` U ) )
14	4 5 3 12	lflcl	|- ( ( U e. LMod /\ F e. ( LFnl ` U ) /\ X e. V ) -> ( F ` X ) e. R )
15	11 13 10 14	syl3anc	|- ( ph -> ( F ` X ) e. R )