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 × 𝑠 S
xpsds.x X = Base R
xpsds.y Y = Base S
xpsds.1 φ R V
xpsds.2 φ S W
xpsds.p P = dist T
xpsds.m M = dist R X × X
xpsds.n N = dist S Y × Y
xpsmet.3 φ M Met X
xpsmet.4 φ N Met Y
Assertion xpsmet φ P Met X × Y

Proof

Step Hyp Ref Expression
1 xpsds.t T = R × 𝑠 S
2 xpsds.x X = Base R
3 xpsds.y Y = Base S
4 xpsds.1 φ R V
5 xpsds.2 φ S W
6 xpsds.p P = dist T
7 xpsds.m M = dist R X × X
8 xpsds.n N = dist S Y × Y
9 xpsmet.3 φ M Met X
10 xpsmet.4 φ N Met Y
11 eqid x X , y Y x 1 𝑜 y = x X , y Y x 1 𝑜 y
12 eqid Scalar R = Scalar R
13 eqid Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 R 1 𝑜 S
14 1 2 3 4 5 11 12 13 xpsval φ T = x X , y Y x 1 𝑜 y -1 𝑠 Scalar R 𝑠 R 1 𝑜 S
15 1 2 3 4 5 11 12 13 xpsrnbas φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 R 1 𝑜 S
16 11 xpsff1o2 x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y
17 f1ocnv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
18 16 17 mp1i φ x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
19 ovexd φ Scalar R 𝑠 R 1 𝑜 S V
20 eqid dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y = dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y
21 eqid Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
22 eqid Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
23 eqid Base R 1 𝑜 S k = Base R 1 𝑜 S k
24 eqid dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k
25 eqid dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
26 fvexd φ Scalar R V
27 2onn 2 𝑜 ω
28 nnfi 2 𝑜 ω 2 𝑜 Fin
29 27 28 mp1i φ 2 𝑜 Fin
30 fvexd φ k 2 𝑜 R 1 𝑜 S k V
31 elpri k 1 𝑜 k = k = 1 𝑜
32 df2o3 2 𝑜 = 1 𝑜
33 31 32 eleq2s k 2 𝑜 k = k = 1 𝑜
34 9 adantr φ k = M Met X
35 fveq2 k = R 1 𝑜 S k = R 1 𝑜 S
36 fvpr0o R V R 1 𝑜 S = R
37 4 36 syl φ R 1 𝑜 S = R
38 35 37 sylan9eqr φ k = R 1 𝑜 S k = R
39 38 fveq2d φ k = dist R 1 𝑜 S k = dist R
40 38 fveq2d φ k = Base R 1 𝑜 S k = Base R
41 40 2 eqtr4di φ k = Base R 1 𝑜 S k = X
42 41 sqxpeqd φ k = Base R 1 𝑜 S k × Base R 1 𝑜 S k = X × X
43 39 42 reseq12d φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist R X × X
44 43 7 eqtr4di φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = M
45 41 fveq2d φ k = Met Base R 1 𝑜 S k = Met X
46 34 44 45 3eltr4d φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k Met Base R 1 𝑜 S k
47 10 adantr φ k = 1 𝑜 N Met Y
48 fveq2 k = 1 𝑜 R 1 𝑜 S k = R 1 𝑜 S 1 𝑜
49 fvpr1o S W R 1 𝑜 S 1 𝑜 = S
50 5 49 syl φ R 1 𝑜 S 1 𝑜 = S
51 48 50 sylan9eqr φ k = 1 𝑜 R 1 𝑜 S k = S
52 51 fveq2d φ k = 1 𝑜 dist R 1 𝑜 S k = dist S
53 51 fveq2d φ k = 1 𝑜 Base R 1 𝑜 S k = Base S
54 53 3 eqtr4di φ k = 1 𝑜 Base R 1 𝑜 S k = Y
55 54 sqxpeqd φ k = 1 𝑜 Base R 1 𝑜 S k × Base R 1 𝑜 S k = Y × Y
56 52 55 reseq12d φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist S Y × Y
57 56 8 eqtr4di φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = N
58 54 fveq2d φ k = 1 𝑜 Met Base R 1 𝑜 S k = Met Y
59 47 57 58 3eltr4d φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k Met Base R 1 𝑜 S k
60 46 59 jaodan φ k = k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k Met Base R 1 𝑜 S k
61 33 60 sylan2 φ k 2 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k Met Base R 1 𝑜 S k
62 21 22 23 24 25 26 29 30 61 prdsmet φ dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k Met Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
63 fnpr2o R V S W R 1 𝑜 S Fn 2 𝑜
64 4 5 63 syl2anc φ R 1 𝑜 S Fn 2 𝑜
65 dffn5 R 1 𝑜 S Fn 2 𝑜 R 1 𝑜 S = k 2 𝑜 R 1 𝑜 S k
66 64 65 sylib φ R 1 𝑜 S = k 2 𝑜 R 1 𝑜 S k
67 66 oveq2d φ Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
68 67 fveq2d φ dist Scalar R 𝑠 R 1 𝑜 S = dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
69 67 fveq2d φ Base Scalar R 𝑠 R 1 𝑜 S = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
70 15 69 eqtrd φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
71 70 fveq2d φ Met ran x X , y Y x 1 𝑜 y = Met Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
72 62 68 71 3eltr4d φ dist Scalar R 𝑠 R 1 𝑜 S Met ran x X , y Y x 1 𝑜 y
73 ssid ran x X , y Y x 1 𝑜 y ran x X , y Y x 1 𝑜 y
74 metres2 dist Scalar R 𝑠 R 1 𝑜 S Met ran x X , y Y x 1 𝑜 y ran x X , y Y x 1 𝑜 y ran x X , y Y x 1 𝑜 y dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y Met ran x X , y Y x 1 𝑜 y
75 72 73 74 sylancl φ dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y Met ran x X , y Y x 1 𝑜 y
76 14 15 18 19 20 6 75 imasf1omet φ P Met X × Y