Theorem lcdvbasess

Description: The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-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 ) )
Assertion	lcdvbasess	|- ( ph -> V C_ 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		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
8		eqid	|- ( LKer ` U ) = ( LKer ` U )
9		eqid	|- { f e. F | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } = { f e. F | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) }
10	1 7 2 3 4 5 8 9 6	lcdvbase	|- ( ph -> V = { f e. F | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
11		ssrab2	|- { f e. F | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } C_ F
12	10 11	eqsstrdi	|- ( ph -> V C_ F )