Step |
Hyp |
Ref |
Expression |
1 |
|
prdsxms.y |
|- Y = ( S Xs_ R ) |
2 |
|
prdsxms.s |
|- ( ph -> S e. W ) |
3 |
|
prdsxms.i |
|- ( ph -> I e. Fin ) |
4 |
|
prdsxms.d |
|- D = ( dist ` Y ) |
5 |
|
prdsxms.b |
|- B = ( Base ` Y ) |
6 |
|
prdsxms.r |
|- ( ph -> R : I --> *MetSp ) |
7 |
|
eqid |
|- ( S Xs_ ( k e. I |-> ( R ` k ) ) ) = ( S Xs_ ( k e. I |-> ( R ` k ) ) ) |
8 |
|
eqid |
|- ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) |
9 |
|
eqid |
|- ( Base ` ( R ` k ) ) = ( Base ` ( R ` k ) ) |
10 |
|
eqid |
|- ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) = ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) |
11 |
|
eqid |
|- ( dist ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) = ( dist ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) |
12 |
6
|
ffvelrnda |
|- ( ( ph /\ k e. I ) -> ( R ` k ) e. *MetSp ) |
13 |
9 10
|
xmsxmet |
|- ( ( R ` k ) e. *MetSp -> ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) e. ( *Met ` ( Base ` ( R ` k ) ) ) ) |
14 |
12 13
|
syl |
|- ( ( ph /\ k e. I ) -> ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) e. ( *Met ` ( Base ` ( R ` k ) ) ) ) |
15 |
7 8 9 10 11 2 3 12 14
|
prdsxmet |
|- ( ph -> ( dist ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) e. ( *Met ` ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) ) |
16 |
6
|
feqmptd |
|- ( ph -> R = ( k e. I |-> ( R ` k ) ) ) |
17 |
16
|
oveq2d |
|- ( ph -> ( S Xs_ R ) = ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) |
18 |
1 17
|
eqtrid |
|- ( ph -> Y = ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) |
19 |
18
|
fveq2d |
|- ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) |
20 |
4 19
|
eqtrid |
|- ( ph -> D = ( dist ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) |
21 |
18
|
fveq2d |
|- ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) |
22 |
5 21
|
eqtrid |
|- ( ph -> B = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) |
23 |
22
|
fveq2d |
|- ( ph -> ( *Met ` B ) = ( *Met ` ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) ) ) |
24 |
15 20 23
|
3eltr4d |
|- ( ph -> D e. ( *Met ` B ) ) |