Theorem lcdvbase

Description: Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbase.h	|- H = ( LHyp ` K )
	lcdvbase.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcdvbase.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvbase.v	|- V = ( Base ` C )
	lcdvbase.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvbase.f	|- F = ( LFnl ` U )
	lcdvbase.l	|- L = ( LKer ` U )
	lcdvbase.b	|- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lcdvbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcdvbase	|- ( ph -> V = B )

Proof

Step	Hyp	Ref	Expression
1		lcdvbase.h	|- H = ( LHyp ` K )
2		lcdvbase.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcdvbase.c	|- C = ( ( LCDual ` K ) ` W )
4		lcdvbase.v	|- V = ( Base ` C )
5		lcdvbase.u	|- U = ( ( DVecH ` K ) ` W )
6		lcdvbase.f	|- F = ( LFnl ` U )
7		lcdvbase.l	|- L = ( LKer ` U )
8		lcdvbase.b	|- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
9		lcdvbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		eqid	|- ( LDual ` U ) = ( LDual ` U )
11	1 2 3 5 6 7 10 9 8	lcdval2	|- ( ph -> C = ( ( LDual ` U ) |`s B ) )
12	11	fveq2d	|- ( ph -> ( Base ` C ) = ( Base ` ( ( LDual ` U ) |`s B ) ) )
13	4 12	syl5eq	|- ( ph -> V = ( Base ` ( ( LDual ` U ) |`s B ) ) )
14		ssrab2	|- { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } C_ F
15	8 14	eqsstri	|- B C_ F
16		eqid	|- ( Base ` ( LDual ` U ) ) = ( Base ` ( LDual ` U ) )
17	1 5 9	dvhlmod	|- ( ph -> U e. LMod )
18	6 10 16 17	ldualvbase	|- ( ph -> ( Base ` ( LDual ` U ) ) = F )
19	15 18	sseqtrrid	|- ( ph -> B C_ ( Base ` ( LDual ` U ) ) )
20		eqid	|- ( ( LDual ` U ) |`s B ) = ( ( LDual ` U ) |`s B )
21	20 16	ressbas2	|- ( B C_ ( Base ` ( LDual ` U ) ) -> B = ( Base ` ( ( LDual ` U ) |`s B ) ) )
22	19 21	syl	|- ( ph -> B = ( Base ` ( ( LDual ` U ) |`s B ) ) )
23	13 22	eqtr4d	|- ( ph -> V = B )