Metamath Proof Explorer


Theorem prdsmslem1

Description: Lemma for prdsms . The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsxms.y
|- Y = ( S Xs_ R )
prdsxms.s
|- ( ph -> S e. W )
prdsxms.i
|- ( ph -> I e. Fin )
prdsxms.d
|- D = ( dist ` Y )
prdsxms.b
|- B = ( Base ` Y )
prdsms.r
|- ( ph -> R : I --> MetSp )
Assertion prdsmslem1
|- ( ph -> D e. ( Met ` B ) )

Proof

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 prdsms.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 msmet
 |-  ( ( 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 prdsmet
 |-  ( 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 ) )