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	|- H = ( LHyp ` K )
	mapddlss.m	|- M = ( ( mapd ` K ) ` W )
	mapddlss.u	|- U = ( ( DVecH ` K ) ` W )
	mapddlss.s	|- S = ( LSubSp ` U )
	mapddlss.d	|- D = ( LDual ` U )
	mapddlss.t	|- T = ( LSubSp ` D )
	mapddlss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapddlss.r	|- ( ph -> R e. S )
Assertion	mapddlssN	|- ( ph -> ( M ` R ) e. T )

Proof

Step	Hyp	Ref	Expression
1		mapddlss.h	|- H = ( LHyp ` K )
2		mapddlss.m	|- M = ( ( mapd ` K ) ` W )
3		mapddlss.u	|- U = ( ( DVecH ` K ) ` W )
4		mapddlss.s	|- S = ( LSubSp ` U )
5		mapddlss.d	|- D = ( LDual ` U )
6		mapddlss.t	|- T = ( LSubSp ` D )
7		mapddlss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		mapddlss.r	|- ( ph -> R e. S )
9		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
10		eqid	|- ( LKer ` U ) = ( LKer ` U )
11		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
12	1 3 4 9 10 11 2 7 8	mapdval	|- ( ph -> ( M ` R ) = { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ R ) } )
13		eqid	|- { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ R ) } = { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ R ) }
14	1 11 3 4 9 10 5 6 13 7 8	lclkrs	|- ( ph -> { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ R ) } e. T )
15	12 14	eqeltrd	|- ( ph -> ( M ` R ) e. T )