Theorem lcdval2

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

	Ref	Expression
Hypotheses	lcdval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcdval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdval.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcdval.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcdval.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcdval.k	$$⊢\phi \to \left(K\in X\wedge W\in H\right)$$
	lcdval2.b	$$⊢B=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
Assertion	lcdval2	$$⊢\phi \to C=D{\upharpoonright }_{𝑠}B$$

Proof

Step	Hyp	Ref	Expression
1		lcdval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcdval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
4		lcdval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		lcdval.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lcdval.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lcdval.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lcdval.k	$$⊢\phi \to \left(K\in X\wedge W\in H\right)$$
9		lcdval2.b	$$⊢B=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
10	1 2 3 4 5 6 7 8	lcdval	$$⊢\phi \to C=D{\upharpoonright }_{𝑠}\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
11	9	oveq2i	$$⊢D{\upharpoonright }_{𝑠}B=D{\upharpoonright }_{𝑠}\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
12	10 11	syl6eqr	$$⊢\phi \to C=D{\upharpoonright }_{𝑠}B$$