Metamath Proof Explorer

Theorem xpsmet

Description: The direct product of two metric spaces. Definition 14-1.5 of Gleason p. 225. (Contributed by NM, 20-Jun-2007) (Revised by Mario Carneiro, 20-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 ) )
xpsmet.3 
|- ( ph -> M e. ( Met ` X ) )
xpsmet.4 
|- ( ph -> N e. ( Met ` Y ) )
Assertion xpsmet 
|- ( 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 xpsmet.3 
 |-  ( ph -> M e. ( Met ` X ) )
10 xpsmet.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 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) )
22 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
23 eqid 
 |-  ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) )
24 eqid 
 |-  ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
25 eqid 
 |-  ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
26 fvexd 
 |-  ( ph -> ( Scalar ` R ) e. _V )
27 2onn 
 |-  2o e. _om
28 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
29 27 28 mp1i 
 |-  ( ph -> 2o e. Fin )
30 fvexd 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) e. _V )
31 elpri 
 |-  ( k e. { (/) , 1o } -> ( k = (/) \/ k = 1o ) )
32 df2o3 
 |-  2o = { (/) , 1o }
33 31 32 eleq2s 
 |-  ( k e. 2o -> ( k = (/) \/ k = 1o ) )
34 9 adantr 
 |-  ( ( ph /\ k = (/) ) -> M e. ( Met ` X ) )
35 fveq2 
 |-  ( k = (/) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) )
36 fvpr0o 
 |-  ( R e. V -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
37 4 36 syl 
 |-  ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
38 35 37 sylan9eqr 
 |-  ( ( ph /\ k = (/) ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = R )
39 38 fveq2d 
 |-  ( ( ph /\ k = (/) ) -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` R ) )
40 38 fveq2d 
 |-  ( ( ph /\ k = (/) ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` R ) )
41 40 2 syl6eqr 
 |-  ( ( ph /\ k = (/) ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = X )
42 41 sqxpeqd 
 |-  ( ( ph /\ k = (/) ) -> ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( X X. X ) )
43 39 42 reseq12d 
 |-  ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` R ) |` ( X X. X ) ) )
44 43 7 syl6eqr 
 |-  ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = M )
45 41 fveq2d 
 |-  ( ( ph /\ k = (/) ) -> ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Met ` X ) )
46 34 44 45 3eltr4d 
 |-  ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
47 10 adantr 
 |-  ( ( ph /\ k = 1o ) -> N e. ( Met ` Y ) )
48 fveq2 
 |-  ( k = 1o -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) )
49 fvpr1o 
 |-  ( S e. W -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
50 5 49 syl 
 |-  ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
51 48 50 sylan9eqr 
 |-  ( ( ph /\ k = 1o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = S )
52 51 fveq2d 
 |-  ( ( ph /\ k = 1o ) -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` S ) )
53 51 fveq2d 
 |-  ( ( ph /\ k = 1o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` S ) )
54 53 3 syl6eqr 
 |-  ( ( ph /\ k = 1o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = Y )
55 54 sqxpeqd 
 |-  ( ( ph /\ k = 1o ) -> ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Y X. Y ) )
56 52 55 reseq12d 
 |-  ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` S ) |` ( Y X. Y ) ) )
57 56 8 syl6eqr 
 |-  ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = N )
58 54 fveq2d 
 |-  ( ( ph /\ k = 1o ) -> ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Met ` Y ) )
59 47 57 58 3eltr4d 
 |-  ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
60 46 59 jaodan 
 |-  ( ( ph /\ ( k = (/) \/ k = 1o ) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
61 33 60 sylan2 
 |-  ( ( ph /\ k e. 2o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
62 21 22 23 24 25 26 29 30 61 prdsmet 
 |-  ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) )
63 fnpr2o 
 |-  ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
64 4 5 63 syl2anc 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
65 dffn5 
 |-  ( { <. (/) , R >. , <. 1o , S >. } Fn 2o <-> { <. (/) , R >. , <. 1o , S >. } = ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) )
66 64 65 sylib 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } = ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) )
67 66 oveq2d 
 |-  ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) )
68 67 fveq2d 
 |-  ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) )
69 67 fveq2d 
 |-  ( ph -> ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) )
70 15 69 eqtrd 
 |-  ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) )
71 70 fveq2d 
 |-  ( ph -> ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) = ( Met ` ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) )
72 62 68 71 3eltr4d 
 |-  ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) )
73 ssid 
 |-  ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
74 metres2 
 |-  ( ( ( 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 >. } ) ) )
75 72 73 74 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 >. } ) ) )
76 14 15 18 19 20 6 75 imasf1omet 
 |-  ( ph -> P e. ( Met ` ( X X. Y ) ) )