Theorem mapdrval

Description: Given a dual subspace R (of functionals with closed kernels), reconstruct the subspace Q that maps to it. (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	mapdrval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdrval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdrval.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdrval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdrval.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	mapdrval.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdrval.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdrval.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	mapdrval.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
	mapdrval.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
	mapdrval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdrval.r	$$⊢\phi \to R\in T$$
	mapdrval.e	$$⊢\phi \to R\subseteq C$$
	mapdrval.q	$$⊢Q=\bigcup _{h\in R}O\left(L\left(h\right)\right)$$
Assertion	mapdrval	$$⊢\phi \to M\left(Q\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		mapdrval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdrval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		mapdrval.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
4		mapdrval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		mapdrval.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
6		mapdrval.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		mapdrval.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		mapdrval.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
9		mapdrval.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
10		mapdrval.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
11		mapdrval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		mapdrval.r	$$⊢\phi \to R\in T$$
13		mapdrval.e	$$⊢\phi \to R\subseteq C$$
14		mapdrval.q	$$⊢Q=\bigcup _{h\in R}O\left(L\left(h\right)\right)$$
15	1 2 4 5 6 7 8 9 10 14 11 12 13	lcfr	$$⊢\phi \to Q\in S$$
16	1 4 5 6 7 2 3 11 15 10	mapdvalc	$$⊢\phi \to M\left(Q\right)=\left\{f\in C|O\left(L\left(f\right)\right)\subseteq Q\right\}$$
17		2fveq3	$$⊢h=i\to O\left(L\left(h\right)\right)=O\left(L\left(i\right)\right)$$
18	17	cbviunv	$$⊢\bigcup _{h\in R}O\left(L\left(h\right)\right)=\bigcup _{i\in R}O\left(L\left(i\right)\right)$$
19	14 18	eqtri	$$⊢Q=\bigcup _{i\in R}O\left(L\left(i\right)\right)$$
20		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
21		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
22		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
23		eqid	$$⊢0_U=0_U$$
24		eqid	$$⊢0_D=0_D$$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 23 24	mapdrvallem3	$$⊢\phi \to \left\{f\in C|O\left(L\left(f\right)\right)\subseteq Q\right\}=R$$
26	16 25	eqtrd	$$⊢\phi \to M\left(Q\right)=R$$