Theorem lcdval2

Description: Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdval.h	|- H = ( LHyp ` K )
	lcdval.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcdval.c	|- C = ( ( LCDual ` K ) ` W )
	lcdval.u	|- U = ( ( DVecH ` K ) ` W )
	lcdval.f	|- F = ( LFnl ` U )
	lcdval.l	|- L = ( LKer ` U )
	lcdval.d	|- D = ( LDual ` U )
	lcdval.k	|- ( ph -> ( K e. X /\ W e. H ) )
	lcdval2.b	|- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
Assertion	lcdval2	|- ( ph -> C = ( D |`s B ) )

Proof

Step	Hyp	Ref	Expression
1		lcdval.h	|- H = ( LHyp ` K )
2		lcdval.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcdval.c	|- C = ( ( LCDual ` K ) ` W )
4		lcdval.u	|- U = ( ( DVecH ` K ) ` W )
5		lcdval.f	|- F = ( LFnl ` U )
6		lcdval.l	|- L = ( LKer ` U )
7		lcdval.d	|- D = ( LDual ` U )
8		lcdval.k	|- ( ph -> ( K e. X /\ W e. H ) )
9		lcdval2.b	|- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
10	1 2 3 4 5 6 7 8	lcdval	|- ( ph -> C = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
11	9	oveq2i	|- ( D |`s B ) = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
12	10 11	eqtr4di	|- ( ph -> C = ( D |`s B ) )