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

Proof

Step	Hyp	Ref	Expression
1		lclkrs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrs.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrs.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		lclkrs.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lclkrs.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lclkrs.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lclkrs.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
9		lclkrs.c	$$⊢C=\left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq R\right)\right\}$$
10		lclkrs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		lclkrs.r	$$⊢\phi \to R\in S$$
12		ssrab2	$$⊢\left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq R\right)\right\}\subseteq F$$
13	12	a1i	$$⊢\phi \to \left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq R\right)\right\}\subseteq F$$
14	9	a1i	$$⊢\phi \to C=\left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq R\right)\right\}$$
15		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
16	1 3 10	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
17	5 7 15 16	ldualvbase	$$⊢\phi \to {\mathrm{Base}}_D=F$$
18	13 14 17	3sstr4d	$$⊢\phi \to C\subseteq {\mathrm{Base}}_D$$
19		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
20		eqid	$$⊢0_{\mathrm{Scalar}\left(U\right)}=0_{\mathrm{Scalar}\left(U\right)}$$
21		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
22	19 20 21 5	lfl0f	$$⊢U\in \mathrm{LMod}\to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F$$
23	16 22	syl	$$⊢\phi \to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in F$$
24	1 3 2 21 10	dochoc1	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)\right)={\mathrm{Base}}_U$$
25		eqidd	$$⊢\phi \to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}$$
26	19 20 21 5 6	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)$$
27	16 23 26	syl2anc	$$⊢\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)$$
28	25 27	mpbird	$$⊢\phi \to L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)={\mathrm{Base}}_U$$
29	28	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)$$
30	29	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)$$
31	24 30 28	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)$$
32		eqid	$$⊢0_U=0_U$$
33	1 3 2 21 32	doch1	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)=\left\{0_U\right\}$$
34	10 33	syl	$$⊢\phi \to \underset{\dot{}}{\perp }\left({\mathrm{Base}}_U\right)=\left\{0_U\right\}$$
35	29 34	eqtrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)=\left\{0_U\right\}$$
36	32 4	lss0ss	$$⊢\left(U\in \mathrm{LMod}\wedge R\in S\right)\to \left\{0_U\right\}\subseteq R$$
37	16 11 36	syl2anc	$$⊢\phi \to \left\{0_U\right\}\subseteq R$$
38	35 37	eqsstrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)\subseteq R$$
39	9	lcfls1lem	$$⊢{\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)\wedge \underset{\dot{}}{\perp }\left(L\left({\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\right)\right)\subseteq R\right)$$
40	23 31 38 39	syl3anbrc	$$⊢\phi \to {\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}\in C$$
41	40	ne0d	$$⊢\phi \to C\ne \varnothing$$
42		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
43		eqid	$$⊢{\cdot }_D={\cdot }_D$$
44	10	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)$$
45	11	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 R\in S$$
46		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$$
47		eqid	$$⊢{+}_D={+}_D$$
48		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$$
49		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)}$$
50		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
51		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
52	19 42 7 50 51 16	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
53	52	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)}$$
54	49 53	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)}$$
55	1 2 3 4 5 6 7 19 42 43 9 44 45 48 54	lclkrslem1	$$⊢\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$$
56	1 2 3 4 5 6 7 19 42 43 9 44 45 46 47 55	lclkrslem2	$$⊢\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$$
57	56	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$$
58	50 51 15 47 43 8	islss	$$⊢C\in T\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)$$
59	18 41 57 58	syl3anbrc	$$⊢\phi \to C\in T$$