Metamath Proof Explorer

Theorem xpsxms

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

Ref Expression
Hypothesis xpsms.t 
|- T = ( R Xs. S )
Assertion xpsxms 
|- ( ( R e. *MetSp /\ S e. *MetSp ) -> T e. *MetSp )

Proof

Step Hyp Ref Expression
1 xpsms.t 
 |-  T = ( R Xs. S )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 simpl 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> R e. *MetSp )
5 simpr 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> S e. *MetSp )
6 eqid 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
7 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
8 eqid 
 |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
9 1 2 3 4 5 6 7 8 xpsval 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> T = ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
10 1 2 3 4 5 6 7 8 xpsrnbas 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
11 6 xpsff1o2 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
12 f1ocnv 
 |-  ( ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
13 11 12 mp1i 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
14 fvexd 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> ( Scalar ` R ) e. _V )
15 2onn 
 |-  2o e. _om
16 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
17 15 16 mp1i 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> 2o e. Fin )
18 xpscf 
 |-  ( { <. (/) , R >. , <. 1o , S >. } : 2o --> *MetSp <-> ( R e. *MetSp /\ S e. *MetSp ) )
19 18 biimpri 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> { <. (/) , R >. , <. 1o , S >. } : 2o --> *MetSp )
20 8 prdsxms 
 |-  ( ( ( Scalar ` R ) e. _V /\ 2o e. Fin /\ { <. (/) , R >. , <. 1o , S >. } : 2o --> *MetSp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. *MetSp )
21 14 17 19 20 syl3anc 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. *MetSp )
22 9 10 13 21 imasf1oxms 
 |-  ( ( R e. *MetSp /\ S e. *MetSp ) -> T e. *MetSp )