Metamath Proof Explorer

Theorem xpsxmet

Description: A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses xpsds.t 
|- T = ( R Xs. S )
xpsds.x 
|- X = ( Base ` R )
xpsds.y 
|- Y = ( Base ` S )
xpsds.1 
|- ( ph -> R e. V )
xpsds.2 
|- ( ph -> S e. W )
xpsds.p 
|- P = ( dist ` T )
xpsds.m 
|- M = ( ( dist ` R ) |` ( X X. X ) )
xpsds.n 
|- N = ( ( dist ` S ) |` ( Y X. Y ) )
xpsds.3 
|- ( ph -> M e. ( *Met ` X ) )
xpsds.4 
|- ( ph -> N e. ( *Met ` Y ) )
Assertion xpsxmet 
|- ( ph -> P e. ( *Met ` ( X X. Y ) ) )

Proof

Step Hyp Ref Expression
1 xpsds.t 
 |-  T = ( R Xs. S )
2 xpsds.x 
 |-  X = ( Base ` R )
3 xpsds.y 
 |-  Y = ( Base ` S )
4 xpsds.1 
 |-  ( ph -> R e. V )
5 xpsds.2 
 |-  ( ph -> S e. W )
6 xpsds.p 
 |-  P = ( dist ` T )
7 xpsds.m 
 |-  M = ( ( dist ` R ) |` ( X X. X ) )
8 xpsds.n 
 |-  N = ( ( dist ` S ) |` ( Y X. Y ) )
9 xpsds.3 
 |-  ( ph -> M e. ( *Met ` X ) )
10 xpsds.4 
 |-  ( ph -> N e. ( *Met ` Y ) )
11 eqid 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
12 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
13 eqid 
 |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
14 1 2 3 4 5 11 12 13 xpsval 
 |-  ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
15 1 2 3 4 5 11 12 13 xpsrnbas 
 |-  ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
16 11 xpsff1o2 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
17 f1ocnv 
 |-  ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
18 16 17 mp1i 
 |-  ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
19 ovexd 
 |-  ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
20 eqid 
 |-  ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) = ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) )
21 1 2 3 4 5 6 7 8 9 10 xpsxmetlem 
 |-  ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) )
22 ssid 
 |-  ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
23 xmetres2 
 |-  ( ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) /\ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) )
24 21 22 23 sylancl 
 |-  ( ph -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) )
25 14 15 18 19 20 6 24 imasf1oxmet 
 |-  ( ph -> P e. ( *Met ` ( X X. Y ) ) )