lclkrs

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace R is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr a special case of this? (Contributed by NM, 29-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lclkrs.h	\|- H = ( LHyp ` K )
2		lclkrs.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
3		lclkrs.u	\|- U = ( ( DVecH ` K ) ` W )
4		lclkrs.s	\|- S = ( LSubSp ` U )
5		lclkrs.f	\|- F = ( LFnl ` U )
6		lclkrs.l	\|- L = ( LKer ` U )
7		lclkrs.d	\|- D = ( LDual ` U )
8		lclkrs.t	\|- T = ( LSubSp ` D )
9		lclkrs.c	\|- C = { f e. F \| ( ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._\|_ ` ( L ` f ) ) C_ R ) }
10		lclkrs.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
11		lclkrs.r	\|- ( ph -> R e. S )
12		ssrab2	\|- { f e. F \| ( ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._\|_ ` ( L ` f ) ) C_ R ) } C_ F
13	12	a1i	\|- ( ph -> { f e. F \| ( ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._\|_ ` ( L ` f ) ) C_ R ) } C_ F )
14	9	a1i	\|- ( ph -> C = { f e. F \| ( ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._\|_ ` ( L ` f ) ) C_ R ) } )
15		eqid	\|- ( Base ` D ) = ( Base ` D )
16	1 3 10	dvhlmod	\|- ( ph -> U e. LMod )
17	5 7 15 16	ldualvbase	\|- ( ph -> ( Base ` D ) = F )
18	13 14 17	3sstr4d	\|- ( ph -> C C_ ( Base ` D ) )
19		eqid	\|- ( Scalar ` U ) = ( Scalar ` U )
20		eqid	\|- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
21		eqid	\|- ( Base ` U ) = ( Base ` U )
22	19 20 21 5	lfl0f	\|- ( U e. LMod -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F )
23	16 22	syl	\|- ( ph -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F )
24	1 3 2 21 10	dochoc1	\|- ( ph -> ( ._\|_ ` ( ._\|_ ` ( Base ` U ) ) ) = ( Base ` U ) )
25		eqidd	\|- ( ph -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
26	19 20 21 5 6	lkr0f	\|- ( ( U e. LMod /\ ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F ) -> ( ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) = ( Base ` U ) <-> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
27	16 23 26	syl2anc	\|- ( ph -> ( ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) = ( Base ` U ) <-> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
28	25 27	mpbird	\|- ( ph -> ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) = ( Base ` U ) )
29	28	fveq2d	\|- ( ph -> ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) = ( ._\|_ ` ( Base ` U ) ) )
30	29	fveq2d	\|- ( ph -> ( ._\|_ ` ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) ) = ( ._\|_ ` ( ._\|_ ` ( Base ` U ) ) ) )
31	24 30 28	3eqtr4d	\|- ( ph -> ( ._\|_ ` ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) ) = ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
32		eqid	\|- ( 0g ` U ) = ( 0g ` U )
33	1 3 2 21 32	doch1	\|- ( ( K e. HL /\ W e. H ) -> ( ._\|_ ` ( Base ` U ) ) = { ( 0g ` U ) } )
34	10 33	syl	\|- ( ph -> ( ._\|_ ` ( Base ` U ) ) = { ( 0g ` U ) } )
35	29 34	eqtrd	\|- ( ph -> ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) = { ( 0g ` U ) } )
36	32 4	lss0ss	\|- ( ( U e. LMod /\ R e. S ) -> { ( 0g ` U ) } C_ R )
37	16 11 36	syl2anc	\|- ( ph -> { ( 0g ` U ) } C_ R )
38	35 37	eqsstrd	\|- ( ph -> ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) C_ R )
39	9	lcfls1lem	\|- ( ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. C <-> ( ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F /\ ( ._\|_ ` ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) ) = ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( ._\|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) C_ R ) )
40	23 31 38 39	syl3anbrc	\|- ( ph -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. C )
41	40	ne0d	\|- ( ph -> C =/= (/) )
42		eqid	\|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
43		eqid	\|- ( .s ` D ) = ( .s ` D )
44	10	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( K e. HL /\ W e. H ) )
45	11	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> R e. S )
46		simpr3	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> b e. C )
47		eqid	\|- ( +g ` D ) = ( +g ` D )
48		simpr2	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> a e. C )
49		simpr1	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> x e. ( Base ` ( Scalar ` D ) ) )
50		eqid	\|- ( Scalar ` D ) = ( Scalar ` D )
51		eqid	\|- ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
52	19 42 7 50 51 16	ldualsbase	\|- ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` U ) ) )
53	52	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` U ) ) )
54	49 53	eleqtrd	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> x e. ( Base ` ( Scalar ` U ) ) )
55	1 2 3 4 5 6 7 19 42 43 9 44 45 48 54	lclkrslem1	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( x ( .s ` D ) a ) e. C )
56	1 2 3 4 5 6 7 19 42 43 9 44 45 46 47 55	lclkrslem2	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( ( x ( .s ` D ) a ) ( +g ` D ) b ) e. C )
57	56	ralrimivvva	\|- ( ph -> A. x e. ( Base ` ( Scalar ` D ) ) A. a e. C A. b e. C ( ( x ( .s ` D ) a ) ( +g ` D ) b ) e. C )
58	50 51 15 47 43 8	islss	\|- ( C e. T <-> ( C C_ ( Base ` D ) /\ C =/= (/) /\ A. x e. ( Base ` ( Scalar ` D ) ) A. a e. C A. b e. C ( ( x ( .s ` D ) a ) ( +g ` D ) b ) e. C ) )
59	18 41 57 58	syl3anbrc	\|- ( ph -> C e. T )

Metamath Proof Explorer

Theorem lclkrs

Proof