Theorem lcdvbase

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

	Ref	Expression
Hypotheses	lcdvbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvbase.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcdvbase.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvbase.v	$$⊢V={\mathrm{Base}}_C$$
	lcdvbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvbase.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcdvbase.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcdvbase.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\}$$
	lcdvbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcdvbase	$$⊢\phi \to V=B$$

Proof

Step	Hyp	Ref	Expression
1		lcdvbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvbase.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcdvbase.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
4		lcdvbase.v	$$⊢V={\mathrm{Base}}_C$$
5		lcdvbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		lcdvbase.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		lcdvbase.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		lcdvbase.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\}$$
9		lcdvbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
11	1 2 3 5 6 7 10 9 8	lcdval2	$$⊢\phi \to C=\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B$$
12	11	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left(\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B\right)}$$
13	4 12	syl5eq	$$⊢\phi \to V={\mathrm{Base}}_{\left(\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B\right)}$$
14		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$$
15	8 14	eqsstri	$$⊢B\subseteq F$$
16		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}={\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}$$
17	1 5 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	6 10 16 17	ldualvbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}=F$$
19	15 18	sseqtrrid	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}$$
20		eqid	$$⊢\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B=\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B$$
21	20 16	ressbas2	$$⊢B\subseteq {\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}\to B={\mathrm{Base}}_{\left(\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B\right)}$$
22	19 21	syl	$$⊢\phi \to B={\mathrm{Base}}_{\left(\mathrm{LDual}\left(U\right){\upharpoonright }_{𝑠}B\right)}$$
23	13 22	eqtr4d	$$⊢\phi \to V=B$$