Theorem mapdcl

Description: Closure the value of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	mapdcnvcl.h	|- H = ( LHyp ` K )
	mapdcnvcl.m	|- M = ( ( mapd ` K ) ` W )
	mapdcnvcl.u	|- U = ( ( DVecH ` K ) ` W )
	mapdcnvcl.s	|- S = ( LSubSp ` U )
	mapdcnvcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdcl.x	|- ( ph -> X e. S )
Assertion	mapdcl	|- ( ph -> ( M ` X ) e. ran M )

Proof

Step	Hyp	Ref	Expression
1		mapdcnvcl.h	|- H = ( LHyp ` K )
2		mapdcnvcl.m	|- M = ( ( mapd ` K ) ` W )
3		mapdcnvcl.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdcnvcl.s	|- S = ( LSubSp ` U )
5		mapdcnvcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		mapdcl.x	|- ( ph -> X e. S )
7		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
8		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
9		eqid	|- ( LKer ` U ) = ( LKer ` U )
10		eqid	|- ( LDual ` U ) = ( LDual ` U )
11		eqid	|- ( LSubSp ` ( LDual ` U ) ) = ( LSubSp ` ( LDual ` U ) )
12		eqid	|- { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) } = { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) }
13	1 7 2 3 4 8 9 10 11 12 5	mapd1o	|- ( ph -> M : S -1-1-onto-> ( ( LSubSp ` ( LDual ` U ) ) i^i ~P { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) } ) )
14		f1ofn	|- ( M : S -1-1-onto-> ( ( LSubSp ` ( LDual ` U ) ) i^i ~P { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) } ) -> M Fn S )
15	13 14	syl	|- ( ph -> M Fn S )
16		dffn3	|- ( M Fn S <-> M : S --> ran M )
17	15 16	sylib	|- ( ph -> M : S --> ran M )
18	17 6	ffvelrnd	|- ( ph -> ( M ` X ) e. ran M )