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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdlss.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	mapdlss.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	mapdlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐶 )
	mapdlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdlss.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
Assertion	mapdcl2	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mapdlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdlss.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapdlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		mapdlss.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		mapdlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐶 )
7		mapdlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		mapdlss.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
9	1 2 3 4 7 8	mapdcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) ∈ ran 𝑀 )
10	1 2 5 6 7	mapdrn2	⊢ ( 𝜑 → ran 𝑀 = 𝑇 )
11	9 10	eleqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) ∈ 𝑇 )