Metamath Proof Explorer

Theorem mapdcnvid2

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

Ref Expression
Hypotheses mapdcnvid2.h 
|- H = ( LHyp ` K )
mapdcnvid2.m 
|- M = ( ( mapd ` K ) ` W )
mapdcnvid2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdcnvid2.x 
|- ( ph -> X e. ran M )
Assertion mapdcnvid2 
|- ( ph -> ( M ` ( `' M ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 mapdcnvid2.h 
 |-  H = ( LHyp ` K )
2 mapdcnvid2.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdcnvid2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 mapdcnvid2.x 
 |-  ( ph -> X e. ran M )
5 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
6 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
7 eqid 
 |-  ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( 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 
 |-  { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) } = { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) }
13 1 5 2 6 7 8 9 10 11 12 3 mapd1o 
 |-  ( ph -> M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-onto-> ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) } ) )
14 f1of1 
 |-  ( M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-onto-> ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) } ) -> M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-> ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) } ) )
15 f1f1orn 
 |-  ( M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-> ( ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) i^i ~P { g e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` g ) } ) -> M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-onto-> ran M )
16 13 14 15 3syl 
 |-  ( ph -> M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-onto-> ran M )
17 f1ocnvfv2 
 |-  ( ( M : ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -1-1-onto-> ran M /\ X e. ran M ) -> ( M ` ( `' M ` X ) ) = X )
18 16 4 17 syl2anc 
 |-  ( ph -> ( M ` ( `' M ` X ) ) = X )