Theorem lcdlss

Description: Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdlss.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcdlss.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdlss.s	$$⊢S=\mathrm{LSubSp}\left(C\right)$$
	lcdlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdlss.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcdlss.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcdlss.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcdlss.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
	lcdlss.b	$$⊢B=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcdlss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcdlss	$$⊢\phi \to S=T\cap 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		lcdlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdlss.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcdlss.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
4		lcdlss.s	$$⊢S=\mathrm{LSubSp}\left(C\right)$$
5		lcdlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		lcdlss.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		lcdlss.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		lcdlss.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
9		lcdlss.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
10		lcdlss.b	$$⊢B=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
11		lcdlss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12	1 2 3 5 6 7 8 11 10	lcdval2	$$⊢\phi \to C=D{\upharpoonright }_{𝑠}B$$
13	12	fveq2d	$$⊢\phi \to \mathrm{LSubSp}\left(C\right)=\mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)$$
14	4 13	eqtrid	$$⊢\phi \to S=\mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)$$
15	14	eleq2d	$$⊢\phi \to \left(u\in S\leftrightarrow u\in \mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)\right)$$
16	1 5 11	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
17	8 16	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
18	1 5 2 6 7 8 9 10 11	lclkr	$$⊢\phi \to B\in T$$
19		eqid	$$⊢D{\upharpoonright }_{𝑠}B=D{\upharpoonright }_{𝑠}B$$
20		eqid	$$⊢\mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)=\mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)$$
21	19 9 20	lsslss	$$⊢\left(D\in \mathrm{LMod}\wedge B\in T\right)\to \left(u\in \mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)\leftrightarrow \left(u\in T\wedge u\subseteq B\right)\right)$$
22	17 18 21	syl2anc	$$⊢\phi \to \left(u\in \mathrm{LSubSp}\left(D{\upharpoonright }_{𝑠}B\right)\leftrightarrow \left(u\in T\wedge u\subseteq B\right)\right)$$
23	15 22	bitrd	$$⊢\phi \to \left(u\in S\leftrightarrow \left(u\in T\wedge u\subseteq B\right)\right)$$
24		elin	$$⊢u\in \left(T\cap 𝒫B\right)\leftrightarrow \left(u\in T\wedge u\in 𝒫B\right)$$
25		velpw	$$⊢u\in 𝒫B\leftrightarrow u\subseteq B$$
26	25	anbi2i	$$⊢\left(u\in T\wedge u\in 𝒫B\right)\leftrightarrow \left(u\in T\wedge u\subseteq B\right)$$
27	24 26	bitr2i	$$⊢\left(u\in T\wedge u\subseteq B\right)\leftrightarrow u\in \left(T\cap 𝒫B\right)$$
28	23 27	bitrdi	$$⊢\phi \to \left(u\in S\leftrightarrow u\in \left(T\cap 𝒫B\right)\right)$$
29	28	eqrdv	$$⊢\phi \to S=T\cap 𝒫B$$