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=\mathrm{LHyp}\left(K\right)$$
	lclkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkr.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkr.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkr.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkr.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkr.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
	lclkr.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lclkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lclkr	$$⊢\phi \to C\in S$$

Proof

Step	Hyp	Ref	Expression
1		lclkr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lclkr.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		lclkr.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
5		lclkr.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
6		lclkr.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
7		lclkr.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
8		lclkr.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
9		lclkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		ssrab2	$$⊢\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}\subseteq F$$
11	10	a1i	$$⊢\phi \to \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}\subseteq F$$
12	8	a1i	$$⊢\phi \to C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
13		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
14	1 2 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
15	4 6 13 14	ldualvbase	$$⊢\phi \to {\mathrm{Base}}_D=F$$
16	11 12 15	3sstr4d	$$⊢\phi \to C\subseteq {\mathrm{Base}}_D$$
17		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
18		eqid	$$⊢0_{\mathrm{Scalar}\left(U\right)}=0_{\mathrm{Scalar}\left(U\right)}$$
19		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
20	17 18 19 4	lfl0f	$$⊢U\in \mathrm{LMod}\to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F$$
21	14 20	syl	$$⊢\phi \to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F$$
22	1 2 3 19 9	dochoc1	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)\right)={\mathrm{Base}}_U$$
23		eqid	$$⊢{\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}$$
24	17 18 19 4 5	lkr0f	$$⊢\left(U\in \mathrm{LMod}\wedge {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F\right)\to \left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)={\mathrm{Base}}_U\leftrightarrow {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)$$
25	14 20 24	syl2anc2	$$⊢\phi \to \left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)={\mathrm{Base}}_U\leftrightarrow {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)$$
26	23 25	mpbiri	$$⊢\phi \to L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)={\mathrm{Base}}_U$$
27	26	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)=\underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)$$
28	27	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)\right)$$
29	22 28 26	3eqtr4d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)\right)=L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)$$
30	8	lcfl1lem	$$⊢{\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in C\leftrightarrow \left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)\right)=L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)$$
31	21 29 30	sylanbrc	$$⊢\phi \to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in C$$
32	31	ne0d	$$⊢\phi \to C\ne \varnothing$$
33		eqid	$$⊢{+}_D={+}_D$$
34	9	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
35		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
36		eqid	$$⊢{\cdot }_D={\cdot }_D$$
37		simpr1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
38		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
39		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
40	17 35 6 38 39 14	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
41	40	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
42	37 41	eleqtrd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
43		simpr2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to a\in C$$
44	1 3 2 4 5 6 17 35 36 8 34 42 43	lclkrlem1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to x{\cdot }_{D}a\in C$$
45		simpr3	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to b\in C$$
46	1 3 2 4 5 6 33 8 34 44 45	lclkrlem2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge a\in C\wedge b\in C\right)\right)\to \left(x{\cdot }_{D}a\right){+}_{D}b\in C$$
47	46	ralrimivvva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\forall a\in C\forall b\in C\left(x{\cdot }_{D}a\right){+}_{D}b\in C$$
48	38 39 13 33 36 7	islss	$$⊢C\in S\leftrightarrow \left(C\subseteq {\mathrm{Base}}_D\wedge C\ne \varnothing \wedge \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\forall a\in C\forall b\in C\left(x{\cdot }_{D}a\right){+}_{D}b\in C\right)$$
49	16 32 47 48	syl3anbrc	$$⊢\phi \to C\in S$$