Metamath Proof Explorer

Theorem prdsms

Description: The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis prdsxms.y 
|- Y = ( S Xs_ R )
Assertion prdsms 
|- ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> Y e. MetSp )

Proof

Step Hyp Ref Expression
1 prdsxms.y 
 |-  Y = ( S Xs_ R )
2 msxms 
 |-  ( x e. MetSp -> x e. *MetSp )
3 2 ssriv 
 |-  MetSp C_ *MetSp
4 fss 
 |-  ( ( R : I --> MetSp /\ MetSp C_ *MetSp ) -> R : I --> *MetSp )
5 3 4 mpan2 
 |-  ( R : I --> MetSp -> R : I --> *MetSp )
6 1 prdsxms 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> Y e. *MetSp )
7 5 6 syl3an3 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> Y e. *MetSp )
8 simp1 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> S e. W )
9 simp2 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> I e. Fin )
10 eqid 
 |-  ( dist ` Y ) = ( dist ` Y )
11 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
12 simp3 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> R : I --> MetSp )
13 1 8 9 10 11 12 prdsmslem1 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> ( dist ` Y ) e. ( Met ` ( Base ` Y ) ) )
14 ssid 
 |-  ( Base ` Y ) C_ ( Base ` Y )
15 metres2 
 |-  ( ( ( dist ` Y ) e. ( Met ` ( Base ` Y ) ) /\ ( Base ` Y ) C_ ( Base ` Y ) ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( Met ` ( Base ` Y ) ) )
16 13 14 15 sylancl 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( Met ` ( Base ` Y ) ) )
17 eqid 
 |-  ( TopOpen ` Y ) = ( TopOpen ` Y )
18 eqid 
 |-  ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) = ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) )
19 17 11 18 isms 
 |-  ( Y e. MetSp <-> ( Y e. *MetSp /\ ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( Met ` ( Base ` Y ) ) ) )
20 7 16 19 sylanbrc 
 |-  ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> Y e. MetSp )