Theorem mapdcl2

Description: The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015)

	Ref	Expression
Hypotheses	mapdlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdlss.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdlss.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	mapdlss.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdlss.t	$$⊢T=\mathrm{LSubSp}\left(C\right)$$
	mapdlss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdlss.r	$$⊢\phi \to R\in S$$
Assertion	mapdcl2	$$⊢\phi \to M\left(R\right)\in T$$

Proof

Step	Hyp	Ref	Expression
1		mapdlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdlss.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdlss.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		mapdlss.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		mapdlss.t	$$⊢T=\mathrm{LSubSp}\left(C\right)$$
7		mapdlss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		mapdlss.r	$$⊢\phi \to R\in S$$
9	1 2 3 4 7 8	mapdcl	$$⊢\phi \to M\left(R\right)\in \mathrm{ran}M$$
10	1 2 5 6 7	mapdrn2	$$⊢\phi \to \mathrm{ran}M=T$$
11	9 10	eleqtrd	$$⊢\phi \to M\left(R\right)\in T$$