Step |
Hyp |
Ref |
Expression |
1 |
|
dihcnvid2.h |
|- H = ( LHyp ` K ) |
2 |
|
dihcnvid2.i |
|- I = ( ( DIsoH ` K ) ` W ) |
3 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
4 |
|
eqid |
|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W ) |
5 |
|
eqid |
|- ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) ) |
6 |
3 1 2 4 5
|
dihf11 |
|- ( ( K e. HL /\ W e. H ) -> I : ( Base ` K ) -1-1-> ( LSubSp ` ( ( DVecH ` K ) ` W ) ) ) |
7 |
|
f1f1orn |
|- ( I : ( Base ` K ) -1-1-> ( LSubSp ` ( ( DVecH ` K ) ` W ) ) -> I : ( Base ` K ) -1-1-onto-> ran I ) |
8 |
6 7
|
syl |
|- ( ( K e. HL /\ W e. H ) -> I : ( Base ` K ) -1-1-onto-> ran I ) |
9 |
|
f1ocnvfv2 |
|- ( ( I : ( Base ` K ) -1-1-onto-> ran I /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X ) |
10 |
8 9
|
sylan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X ) |