Theorem mapdcnvid1N

Description: Converse of the value of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	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	mapdcnvid1N	|- ( ph -> ( `' M ` ( M ` X ) ) = X )

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		f1ocnvfv1	|- ( ( 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 ) } ) /\ X e. S ) -> ( `' M ` ( M ` X ) ) = X )
15	13 6 14	syl2anc	|- ( ph -> ( `' M ` ( M ` X ) ) = X )