Theorem mapdrn

Description: Range of the map defined by df-mapd . (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	mapdrn.h	|- H = ( LHyp ` K )
	mapdrn.o	|- O = ( ( ocH ` K ) ` W )
	mapdrn.m	|- M = ( ( mapd ` K ) ` W )
	mapdrn.u	|- U = ( ( DVecH ` K ) ` W )
	mapdrn.f	|- F = ( LFnl ` U )
	mapdrn.l	|- L = ( LKer ` U )
	mapdrn.d	|- D = ( LDual ` U )
	mapdrn.t	|- T = ( LSubSp ` D )
	mapdrn.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
	mapdrn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	mapdrn	|- ( ph -> ran M = ( T i^i ~P C ) )

Proof

Step	Hyp	Ref	Expression
1		mapdrn.h	|- H = ( LHyp ` K )
2		mapdrn.o	|- O = ( ( ocH ` K ) ` W )
3		mapdrn.m	|- M = ( ( mapd ` K ) ` W )
4		mapdrn.u	|- U = ( ( DVecH ` K ) ` W )
5		mapdrn.f	|- F = ( LFnl ` U )
6		mapdrn.l	|- L = ( LKer ` U )
7		mapdrn.d	|- D = ( LDual ` U )
8		mapdrn.t	|- T = ( LSubSp ` D )
9		mapdrn.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
10		mapdrn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
12	1 2 3 4 11 5 6 7 8 9 10	mapd1o	|- ( ph -> M : ( LSubSp ` U ) -1-1-onto-> ( T i^i ~P C ) )
13		f1ofo	|- ( M : ( LSubSp ` U ) -1-1-onto-> ( T i^i ~P C ) -> M : ( LSubSp ` U ) -onto-> ( T i^i ~P C ) )
14		forn	|- ( M : ( LSubSp ` U ) -onto-> ( T i^i ~P C ) -> ran M = ( T i^i ~P C ) )
15	12 13 14	3syl	|- ( ph -> ran M = ( T i^i ~P C ) )