Theorem lclkrs2

Description: The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace Q is a subspace of the dual space containing functionals with closed kernels. Note that R is the value given by mapdval . (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	lclkrs2.h	|- H = ( LHyp ` K )
	lclkrs2.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lclkrs2.u	|- U = ( ( DVecH ` K ) ` W )
	lclkrs2.s	|- S = ( LSubSp ` U )
	lclkrs2.f	|- F = ( LFnl ` U )
	lclkrs2.l	|- L = ( LKer ` U )
	lclkrs2.d	|- D = ( LDual ` U )
	lclkrs2.t	|- T = ( LSubSp ` D )
	lclkrs2.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lclkrs2.r	|- R = { g e. F | ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) }
	lclkrs2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lclkrs2.q	|- ( ph -> Q e. S )
Assertion	lclkrs2	|- ( ph -> ( R e. T /\ R C_ C ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrs2.h	|- H = ( LHyp ` K )
2		lclkrs2.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lclkrs2.u	|- U = ( ( DVecH ` K ) ` W )
4		lclkrs2.s	|- S = ( LSubSp ` U )
5		lclkrs2.f	|- F = ( LFnl ` U )
6		lclkrs2.l	|- L = ( LKer ` U )
7		lclkrs2.d	|- D = ( LDual ` U )
8		lclkrs2.t	|- T = ( LSubSp ` D )
9		lclkrs2.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
10		lclkrs2.r	|- R = { g e. F | ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) }
11		lclkrs2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
12		lclkrs2.q	|- ( ph -> Q e. S )
13	1 2 3 4 5 6 7 8 10 11 12	lclkrs	|- ( ph -> R e. T )
14		simpl	|- ( ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) -> ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) )
15	14	a1i	|- ( g e. F -> ( ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) -> ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) ) )
16	15	ss2rabi	|- { g e. F | ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) } C_ { g e. F | ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) }
17		fveq2	|- ( f = g -> ( L ` f ) = ( L ` g ) )
18	17	fveq2d	|- ( f = g -> ( ._|_ ` ( L ` f ) ) = ( ._|_ ` ( L ` g ) ) )
19	18	fveq2d	|- ( f = g -> ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) )
20	19 17	eqeq12d	|- ( f = g -> ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) <-> ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) ) )
21	20	cbvrabv	|- { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { g e. F | ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) }
22	9 21	eqtri	|- C = { g e. F | ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) }
23	16 10 22	3sstr4i	|- R C_ C
24	13 23	jctir	|- ( ph -> ( R e. T /\ R C_ C ) )