Theorem mapdcnvcl

Description: Closure of the converse 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 ) )
	mapdcnvcl.x	|- ( ph -> X e. ran M )
Assertion	mapdcnvcl	|- ( ph -> ( `' M ` X ) e. S )

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		mapdcnvcl.x	|- ( ph -> X e. ran M )
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		f1of1	|- ( 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 : S -1-1-> ( ( LSubSp ` ( LDual ` U ) ) i^i ~P { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) } ) )
15		f1f1orn	|- ( M : S -1-1-> ( ( LSubSp ` ( LDual ` U ) ) i^i ~P { g e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) } ) -> M : S -1-1-onto-> ran M )
16	13 14 15	3syl	|- ( ph -> M : S -1-1-onto-> ran M )
17		f1ocnvdm	|- ( ( M : S -1-1-onto-> ran M /\ X e. ran M ) -> ( `' M ` X ) e. S )
18	16 6 17	syl2anc	|- ( ph -> ( `' M ` X ) e. S )