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 = ( LHyp ` K )
	mapdlss.m	|- M = ( ( mapd ` K ) ` W )
	mapdlss.u	|- U = ( ( DVecH ` K ) ` W )
	mapdlss.s	|- S = ( LSubSp ` U )
	mapdlss.c	|- C = ( ( LCDual ` K ) ` W )
	mapdlss.t	|- T = ( LSubSp ` C )
	mapdlss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdlss.r	|- ( ph -> R e. S )
Assertion	mapdcl2	|- ( ph -> ( M ` R ) e. T )

Proof

Step	Hyp	Ref	Expression
1		mapdlss.h	|- H = ( LHyp ` K )
2		mapdlss.m	|- M = ( ( mapd ` K ) ` W )
3		mapdlss.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdlss.s	|- S = ( LSubSp ` U )
5		mapdlss.c	|- C = ( ( LCDual ` K ) ` W )
6		mapdlss.t	|- T = ( LSubSp ` C )
7		mapdlss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		mapdlss.r	|- ( ph -> R e. S )
9	1 2 3 4 7 8	mapdcl	|- ( ph -> ( M ` R ) e. ran M )
10	1 2 5 6 7	mapdrn2	|- ( ph -> ran M = T )
11	9 10	eleqtrd	|- ( ph -> ( M ` R ) e. T )