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 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 ) )