Theorem lcdlss2N

Description: Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcdlss2.h	|- H = ( LHyp ` K )
	lcdlss2.c	|- C = ( ( LCDual ` K ) ` W )
	lcdlss2.s	|- S = ( LSubSp ` C )
	lcdlss2.v	|- V = ( Base ` C )
	lcdlss2.u	|- U = ( ( DVecH ` K ) ` W )
	lcdlss2.d	|- D = ( LDual ` U )
	lcdlss2.t	|- T = ( LSubSp ` D )
	lcdlss2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcdlss2N	|- ( ph -> S = ( T i^i ~P V ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlss2.h	|- H = ( LHyp ` K )
2		lcdlss2.c	|- C = ( ( LCDual ` K ) ` W )
3		lcdlss2.s	|- S = ( LSubSp ` C )
4		lcdlss2.v	|- V = ( Base ` C )
5		lcdlss2.u	|- U = ( ( DVecH ` K ) ` W )
6		lcdlss2.d	|- D = ( LDual ` U )
7		lcdlss2.t	|- T = ( LSubSp ` D )
8		lcdlss2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
10		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
11		eqid	|- ( LKer ` U ) = ( LKer ` U )
12		eqid	|- { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) }
13	1 9 2 3 5 10 11 6 7 12 8	lcdlss	|- ( ph -> S = ( T i^i ~P { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
14	1 9 2 4 5 10 11 12 8	lcdvbase	|- ( ph -> V = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
15	14	pweqd	|- ( ph -> ~P V = ~P { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
16	15	ineq2d	|- ( ph -> ( T i^i ~P V ) = ( T i^i ~P { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
17	13 16	eqtr4d	|- ( ph -> S = ( T i^i ~P V ) )