Theorem mapdrn2

Description: Range of the map defined by df-mapd . TODO: this seems to be needed a lot in hdmaprnlem3eN etc. Would it be better to change df-mapd theorems to use LSubSpC instead of ran M ? (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	mapdrn2.h	|- H = ( LHyp ` K )
	mapdrn2.m	|- M = ( ( mapd ` K ) ` W )
	mapdrn2.c	|- C = ( ( LCDual ` K ) ` W )
	mapdrn2.t	|- T = ( LSubSp ` C )
	mapdrn2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	mapdrn2	|- ( ph -> ran M = T )

Proof

Step	Hyp	Ref	Expression
1		mapdrn2.h	|- H = ( LHyp ` K )
2		mapdrn2.m	|- M = ( ( mapd ` K ) ` W )
3		mapdrn2.c	|- C = ( ( LCDual ` K ) ` W )
4		mapdrn2.t	|- T = ( LSubSp ` C )
5		mapdrn2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
7		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
8		eqid	|- ( LFnl ` ( ( DVecH ` K ) ` W ) ) = ( LFnl ` ( ( DVecH ` K ) ` W ) )
9		eqid	|- ( LKer ` ( ( DVecH ` K ) ` W ) ) = ( LKer ` ( ( DVecH ` K ) ` W ) )
10		eqid	|- ( LDual ` ( ( DVecH ` K ) ` W ) ) = ( LDual ` ( ( DVecH ` K ) ` W ) )
11		eqid	|- ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) = ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) )
12		eqid	|- { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } = { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) }
13	1 6 2 7 8 9 10 11 12 5	mapdrn	|- ( ph -> ran M = ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) )
14	1 6 3 4 7 8 9 10 11 12 5	lcdlss	|- ( ph -> T = ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) )
15	13 14	eqtr4d	|- ( ph -> ran M = T )