Theorem mapddlssN

Description: The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 instead. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapddlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapddlss.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapddlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapddlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	mapddlss.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	mapddlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	mapddlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapddlss.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
Assertion	mapddlssN	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mapddlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapddlss.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapddlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapddlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		mapddlss.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
6		mapddlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
7		mapddlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		mapddlss.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
9		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
10		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
11		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
12	1 3 4 9 10 11 2 7 8	mapdval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ 𝑅 ) } )
13		eqid	⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ 𝑅 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ 𝑅 ) }
14	1 11 3 4 9 10 5 6 13 7 8	lclkrs	⊢ ( 𝜑 → { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ 𝑅 ) } ∈ 𝑇 )
15	12 14	eqeltrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑅 ) ∈ 𝑇 )