Step |
Hyp |
Ref |
Expression |
1 |
|
dibval.b |
|- B = ( Base ` K ) |
2 |
|
dibval.h |
|- H = ( LHyp ` K ) |
3 |
|
dibval.t |
|- T = ( ( LTrn ` K ) ` W ) |
4 |
|
dibval.o |
|- .0. = ( f e. T |-> ( _I |` B ) ) |
5 |
|
dibval.j |
|- J = ( ( DIsoA ` K ) ` W ) |
6 |
|
dibval.i |
|- I = ( ( DIsoB ` K ) ` W ) |
7 |
1 2 3 4 5 6
|
dibfval |
|- ( ( K e. V /\ W e. H ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ) |
8 |
7
|
adantr |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ) |
9 |
8
|
fveq1d |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) ) |
10 |
|
fveq2 |
|- ( x = X -> ( J ` x ) = ( J ` X ) ) |
11 |
10
|
xpeq1d |
|- ( x = X -> ( ( J ` x ) X. { .0. } ) = ( ( J ` X ) X. { .0. } ) ) |
12 |
|
eqid |
|- ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) |
13 |
|
fvex |
|- ( J ` X ) e. _V |
14 |
|
snex |
|- { .0. } e. _V |
15 |
13 14
|
xpex |
|- ( ( J ` X ) X. { .0. } ) e. _V |
16 |
11 12 15
|
fvmpt |
|- ( X e. dom J -> ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) = ( ( J ` X ) X. { .0. } ) ) |
17 |
16
|
adantl |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) = ( ( J ` X ) X. { .0. } ) ) |
18 |
9 17
|
eqtrd |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) ) |