Step |
Hyp |
Ref |
Expression |
1 |
|
dibcl.h |
|- H = ( LHyp ` K ) |
2 |
|
dibcl.i |
|- I = ( ( DIsoB ` K ) ` W ) |
3 |
|
relxp |
|- Rel ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) |
4 |
|
eqid |
|- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W ) |
5 |
1 4 2
|
dibdiadm |
|- ( ( K e. V /\ W e. H ) -> dom I = dom ( ( DIsoA ` K ) ` W ) ) |
6 |
5
|
eleq2d |
|- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> X e. dom ( ( DIsoA ` K ) ` W ) ) ) |
7 |
6
|
biimpa |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X e. dom ( ( DIsoA ` K ) ` W ) ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
10 |
|
eqid |
|- ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) |
11 |
8 1 9 10 4 2
|
dibval |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom ( ( DIsoA ` K ) ` W ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) |
12 |
7 11
|
syldan |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) |
13 |
12
|
releqd |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( Rel ( I ` X ) <-> Rel ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) ) |
14 |
3 13
|
mpbiri |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> Rel ( I ` X ) ) |
15 |
|
rel0 |
|- Rel (/) |
16 |
|
ndmfv |
|- ( -. X e. dom I -> ( I ` X ) = (/) ) |
17 |
16
|
releqd |
|- ( -. X e. dom I -> ( Rel ( I ` X ) <-> Rel (/) ) ) |
18 |
15 17
|
mpbiri |
|- ( -. X e. dom I -> Rel ( I ` X ) ) |
19 |
18
|
adantl |
|- ( ( ( K e. V /\ W e. H ) /\ -. X e. dom I ) -> Rel ( I ` X ) ) |
20 |
14 19
|
pm2.61dan |
|- ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) ) |