Metamath Proof Explorer

Theorem pwsms

Description: A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis pwsms.y 
|- Y = ( R ^s I )
Assertion pwsms 
|- ( ( R e. MetSp /\ I e. Fin ) -> Y e. MetSp )

Proof

Step Hyp Ref Expression
1 pwsms.y 
 |-  Y = ( R ^s I )
2 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
3 1 2 pwsval 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
4 fvexd 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> ( Scalar ` R ) e. _V )
5 simpr 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> I e. Fin )
6 fconst6g 
 |-  ( R e. MetSp -> ( I X. { R } ) : I --> MetSp )
7 6 adantr 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> ( I X. { R } ) : I --> MetSp )
8 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
9 8 prdsms 
 |-  ( ( ( Scalar ` R ) e. _V /\ I e. Fin /\ ( I X. { R } ) : I --> MetSp ) -> ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) e. MetSp )
10 4 5 7 9 syl3anc 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) e. MetSp )
11 3 10 eqeltrd 
 |-  ( ( R e. MetSp /\ I e. Fin ) -> Y e. MetSp )