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

Proof

Step	Hyp	Ref	Expression
1		lclkrs2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrs2.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrs2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrs2.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		lclkrs2.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lclkrs2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lclkrs2.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lclkrs2.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
9		lclkrs2.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\}$$
10		lclkrs2.r	$$⊢R=\left\{g\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\wedge \underset{\dot{}}{\perp }\left(L\left(g\right)\right)\subseteq Q\right)\right\}$$
11		lclkrs2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		lclkrs2.q	$$⊢\phi \to Q\in S$$
13	1 2 3 4 5 6 7 8 10 11 12	lclkrs	$$⊢\phi \to R\in T$$
14		simpl	$$⊢\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\wedge \underset{\dot{}}{\perp }\left(L\left(g\right)\right)\subseteq Q\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)$$
15	14	a1i	$$⊢g\in F\to \left(\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\wedge \underset{\dot{}}{\perp }\left(L\left(g\right)\right)\subseteq Q\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right)$$
16	15	ss2rabi	$$⊢\left\{g\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\wedge \underset{\dot{}}{\perp }\left(L\left(g\right)\right)\subseteq Q\right)\right\}\subseteq \left\{g\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
17		fveq2	$$⊢f=g\to L\left(f\right)=L\left(g\right)$$
18	17	fveq2d	$$⊢f=g\to \underset{\dot{}}{\perp }\left(L\left(f\right)\right)=\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
19	18	fveq2d	$$⊢f=g\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)$$
20	19 17	eqeq12d	$$⊢f=g\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right)$$
21	20	cbvrabv	$$⊢\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}=\left\{g\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
22	9 21	eqtri	$$⊢C=\left\{g\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
23	16 10 22	3sstr4i	$$⊢R\subseteq C$$
24	13 23	jctir	$$⊢\phi \to \left(R\in T\wedge R\subseteq C\right)$$