Theorem lclkr

Description: The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of Holland95 p. 218, line 20, stating "The f_M that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lclkr.h	|- H = ( LHyp ` K )
2		lclkr.u	|- U = ( ( DVecH ` K ) ` W )
3		lclkr.o	|- ._|_ = ( ( ocH ` K ) ` W )
4		lclkr.f	|- F = ( LFnl ` U )
5		lclkr.l	|- L = ( LKer ` U )
6		lclkr.d	|- D = ( LDual ` U )
7		lclkr.s	|- S = ( LSubSp ` D )
8		lclkr.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
9		lclkr.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		ssrab2	|- { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } C_ F
11	10	a1i	|- ( ph -> { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } C_ F )
12	8	a1i	|- ( ph -> C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
13		eqid	|- ( Base ` D ) = ( Base ` D )
14	1 2 9	dvhlmod	|- ( ph -> U e. LMod )
15	4 6 13 14	ldualvbase	|- ( ph -> ( Base ` D ) = F )
16	11 12 15	3sstr4d	|- ( ph -> C C_ ( Base ` D ) )
17		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
18		eqid	|- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
19		eqid	|- ( Base ` U ) = ( Base ` U )
20	17 18 19 4	lfl0f	|- ( U e. LMod -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F )
21	14 20	syl	|- ( ph -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. F )
22	1 2 3 19 9	dochoc1	|- ( ph -> ( ._|_ ` ( ._|_ ` ( Base ` U ) ) ) = ( Base ` U ) )
23		eqid	|- ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } )
24	17 18 19 4 5	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 ) ) } ) ) )
25	14 20 24	syl2anc2	|- ( ph -> ( ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) = ( Base ` U ) <-> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
26	23 25	mpbiri	|- ( ph -> ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) = ( Base ` U ) )
27	26	fveq2d	|- ( ph -> ( ._|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) = ( ._|_ ` ( Base ` U ) ) )
28	27	fveq2d	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) ) = ( ._|_ ` ( ._|_ ` ( Base ` U ) ) ) )
29	22 28 26	3eqtr4d	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) ) ) = ( L ` ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
30	8	lcfl1lem	|- ( ( ( 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 ) ) } ) ) ) )
31	21 29 30	sylanbrc	|- ( ph -> ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) e. C )
32	31	ne0d	|- ( ph -> C =/= (/) )
33		eqid	|- ( +g ` D ) = ( +g ` D )
34	9	adantr	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( K e. HL /\ W e. H ) )
35		eqid	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
36		eqid	|- ( .s ` D ) = ( .s ` D )
37		simpr1	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> x e. ( Base ` ( Scalar ` D ) ) )
38		eqid	|- ( Scalar ` D ) = ( Scalar ` D )
39		eqid	|- ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
40	17 35 6 38 39 14	ldualsbase	|- ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` U ) ) )
41	40	adantr	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` U ) ) )
42	37 41	eleqtrd	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> x e. ( Base ` ( Scalar ` U ) ) )
43		simpr2	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> a e. C )
44	1 3 2 4 5 6 17 35 36 8 34 42 43	lclkrlem1	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( x ( .s ` D ) a ) e. C )
45		simpr3	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> b e. C )
46	1 3 2 4 5 6 33 8 34 44 45	lclkrlem2	|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` D ) ) /\ a e. C /\ b e. C ) ) -> ( ( x ( .s ` D ) a ) ( +g ` D ) b ) e. C )
47	46	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 )
48	38 39 13 33 36 7	islss	|- ( C e. S <-> ( 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 ) )
49	16 32 47 48	syl3anbrc	|- ( ph -> C e. S )