Step |
Hyp |
Ref |
Expression |
1 |
|
diafn.b |
|- B = ( Base ` K ) |
2 |
|
diafn.l |
|- .<_ = ( le ` K ) |
3 |
|
diafn.h |
|- H = ( LHyp ` K ) |
4 |
|
diafn.i |
|- I = ( ( DIsoA ` K ) ` W ) |
5 |
|
fvex |
|- ( ( LTrn ` K ) ` W ) e. _V |
6 |
5
|
rabex |
|- { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } e. _V |
7 |
|
eqid |
|- ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) = ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) |
8 |
6 7
|
fnmpti |
|- ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) Fn { x e. B | x .<_ W } |
9 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
10 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
11 |
1 2 3 9 10 4
|
diafval |
|- ( ( K e. V /\ W e. H ) -> I = ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) ) |
12 |
11
|
fneq1d |
|- ( ( K e. V /\ W e. H ) -> ( I Fn { x e. B | x .<_ W } <-> ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) Fn { x e. B | x .<_ W } ) ) |
13 |
8 12
|
mpbiri |
|- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } ) |