Metamath Proof Explorer


Theorem xpsdsval

Description: Value of the metric in a binary structure product. (Contributed 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
xpsds.3 φ M ∞Met X
xpsds.4 φ N ∞Met Y
xpsds.a φ A X
xpsds.b φ B Y
xpsds.c φ C X
xpsds.d φ D Y
Assertion xpsdsval φ A B P C D = sup A M C B N D * <

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 xpsds.3 φ M ∞Met X
10 xpsds.4 φ N ∞Met Y
11 xpsds.a φ A X
12 xpsds.b φ B Y
13 xpsds.c φ C X
14 xpsds.d φ D Y
15 eqid x X , y Y x 1 𝑜 y = x X , y Y x 1 𝑜 y
16 eqid Scalar R = Scalar R
17 eqid Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 R 1 𝑜 S
18 1 2 3 4 5 15 16 17 xpsval φ T = x X , y Y x 1 𝑜 y -1 𝑠 Scalar R 𝑠 R 1 𝑜 S
19 1 2 3 4 5 15 16 17 xpsrnbas φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 R 1 𝑜 S
20 15 xpsff1o2 x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y
21 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
22 20 21 mp1i φ x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
23 ovexd φ Scalar R 𝑠 R 1 𝑜 S V
24 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
25 1 2 3 4 5 6 7 8 9 10 xpsxmetlem φ dist Scalar R 𝑠 R 1 𝑜 S ∞Met ran x X , y Y x 1 𝑜 y
26 ssid ran x X , y Y x 1 𝑜 y ran x X , y Y x 1 𝑜 y
27 xmetres2 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
28 25 26 27 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
29 df-ov A x X , y Y x 1 𝑜 y B = x X , y Y x 1 𝑜 y A B
30 15 xpsfval A X B Y A x X , y Y x 1 𝑜 y B = A 1 𝑜 B
31 11 12 30 syl2anc φ A x X , y Y x 1 𝑜 y B = A 1 𝑜 B
32 29 31 eqtr3id φ x X , y Y x 1 𝑜 y A B = A 1 𝑜 B
33 11 12 opelxpd φ A B X × Y
34 f1of 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 : X × Y ran x X , y Y x 1 𝑜 y
35 20 34 ax-mp x X , y Y x 1 𝑜 y : X × Y ran x X , y Y x 1 𝑜 y
36 35 ffvelrni A B X × Y x X , y Y x 1 𝑜 y A B ran x X , y Y x 1 𝑜 y
37 33 36 syl φ x X , y Y x 1 𝑜 y A B ran x X , y Y x 1 𝑜 y
38 32 37 eqeltrrd φ A 1 𝑜 B ran x X , y Y x 1 𝑜 y
39 df-ov C x X , y Y x 1 𝑜 y D = x X , y Y x 1 𝑜 y C D
40 15 xpsfval C X D Y C x X , y Y x 1 𝑜 y D = C 1 𝑜 D
41 13 14 40 syl2anc φ C x X , y Y x 1 𝑜 y D = C 1 𝑜 D
42 39 41 eqtr3id φ x X , y Y x 1 𝑜 y C D = C 1 𝑜 D
43 13 14 opelxpd φ C D X × Y
44 35 ffvelrni C D X × Y x X , y Y x 1 𝑜 y C D ran x X , y Y x 1 𝑜 y
45 43 44 syl φ x X , y Y x 1 𝑜 y C D ran x X , y Y x 1 𝑜 y
46 42 45 eqeltrrd φ C 1 𝑜 D ran x X , y Y x 1 𝑜 y
47 18 19 22 23 24 6 28 38 46 imasdsf1o φ x X , y Y x 1 𝑜 y -1 A 1 𝑜 B P x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y C 1 𝑜 D
48 38 46 ovresd φ A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S ran x X , y Y x 1 𝑜 y × ran x X , y Y x 1 𝑜 y C 1 𝑜 D = A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S C 1 𝑜 D
49 47 48 eqtrd φ x X , y Y x 1 𝑜 y -1 A 1 𝑜 B P x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S C 1 𝑜 D
50 f1ocnvfv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y A B X × Y x X , y Y x 1 𝑜 y A B = A 1 𝑜 B x X , y Y x 1 𝑜 y -1 A 1 𝑜 B = A B
51 20 33 50 sylancr φ x X , y Y x 1 𝑜 y A B = A 1 𝑜 B x X , y Y x 1 𝑜 y -1 A 1 𝑜 B = A B
52 32 51 mpd φ x X , y Y x 1 𝑜 y -1 A 1 𝑜 B = A B
53 f1ocnvfv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y C D X × Y x X , y Y x 1 𝑜 y C D = C 1 𝑜 D x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = C D
54 20 43 53 sylancr φ x X , y Y x 1 𝑜 y C D = C 1 𝑜 D x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = C D
55 42 54 mpd φ x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = C D
56 52 55 oveq12d φ x X , y Y x 1 𝑜 y -1 A 1 𝑜 B P x X , y Y x 1 𝑜 y -1 C 1 𝑜 D = A B P C D
57 eqid Base Scalar R 𝑠 R 1 𝑜 S = Base Scalar R 𝑠 R 1 𝑜 S
58 fvexd φ Scalar R V
59 2on 2 𝑜 On
60 59 a1i φ 2 𝑜 On
61 fnpr2o R V S W R 1 𝑜 S Fn 2 𝑜
62 4 5 61 syl2anc φ R 1 𝑜 S Fn 2 𝑜
63 38 19 eleqtrd φ A 1 𝑜 B Base Scalar R 𝑠 R 1 𝑜 S
64 46 19 eleqtrd φ C 1 𝑜 D Base Scalar R 𝑠 R 1 𝑜 S
65 eqid dist Scalar R 𝑠 R 1 𝑜 S = dist Scalar R 𝑠 R 1 𝑜 S
66 17 57 58 60 62 63 64 65 prdsdsval φ A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S C 1 𝑜 D = sup ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k 0 * <
67 df2o3 2 𝑜 = 1 𝑜
68 67 rexeqi k 2 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k k 1 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k
69 0ex V
70 1oex 1 𝑜 V
71 2fveq3 k = dist R 1 𝑜 S k = dist R 1 𝑜 S
72 fveq2 k = A 1 𝑜 B k = A 1 𝑜 B
73 fveq2 k = C 1 𝑜 D k = C 1 𝑜 D
74 71 72 73 oveq123d k = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D
75 74 eqeq2d k = x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D
76 2fveq3 k = 1 𝑜 dist R 1 𝑜 S k = dist R 1 𝑜 S 1 𝑜
77 fveq2 k = 1 𝑜 A 1 𝑜 B k = A 1 𝑜 B 1 𝑜
78 fveq2 k = 1 𝑜 C 1 𝑜 D k = C 1 𝑜 D 1 𝑜
79 76 77 78 oveq123d k = 1 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜
80 79 eqeq2d k = 1 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜
81 69 70 75 80 rexpr k 1 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D x = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜
82 68 81 bitri k 2 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D x = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜
83 fvpr0o R V R 1 𝑜 S = R
84 4 83 syl φ R 1 𝑜 S = R
85 84 fveq2d φ dist R 1 𝑜 S = dist R
86 fvpr0o A X A 1 𝑜 B = A
87 11 86 syl φ A 1 𝑜 B = A
88 fvpr0o C X C 1 𝑜 D = C
89 13 88 syl φ C 1 𝑜 D = C
90 85 87 89 oveq123d φ A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D = A dist R C
91 7 oveqi A M C = A dist R X × X C
92 11 13 ovresd φ A dist R X × X C = A dist R C
93 91 92 syl5eq φ A M C = A dist R C
94 90 93 eqtr4d φ A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D = A M C
95 94 eqeq2d φ x = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D x = A M C
96 fvpr1o S W R 1 𝑜 S 1 𝑜 = S
97 5 96 syl φ R 1 𝑜 S 1 𝑜 = S
98 97 fveq2d φ dist R 1 𝑜 S 1 𝑜 = dist S
99 fvpr1o B Y A 1 𝑜 B 1 𝑜 = B
100 12 99 syl φ A 1 𝑜 B 1 𝑜 = B
101 fvpr1o D Y C 1 𝑜 D 1 𝑜 = D
102 14 101 syl φ C 1 𝑜 D 1 𝑜 = D
103 98 100 102 oveq123d φ A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜 = B dist S D
104 8 oveqi B N D = B dist S Y × Y D
105 12 14 ovresd φ B dist S Y × Y D = B dist S D
106 104 105 syl5eq φ B N D = B dist S D
107 103 106 eqtr4d φ A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜 = B N D
108 107 eqeq2d φ x = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜 x = B N D
109 95 108 orbi12d φ x = A 1 𝑜 B dist R 1 𝑜 S C 1 𝑜 D x = A 1 𝑜 B 1 𝑜 dist R 1 𝑜 S 1 𝑜 C 1 𝑜 D 1 𝑜 x = A M C x = B N D
110 82 109 syl5bb φ k 2 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x = A M C x = B N D
111 eqid k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k = k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k
112 111 elrnmpt x V x ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k k 2 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k
113 112 elv x ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k k 2 𝑜 x = A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k
114 vex x V
115 114 elpr x A M C B N D x = A M C x = B N D
116 110 113 115 3bitr4g φ x ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k x A M C B N D
117 116 eqrdv φ ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k = A M C B N D
118 117 uneq1d φ ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k 0 = A M C B N D 0
119 uncom A M C B N D 0 = 0 A M C B N D
120 118 119 eqtrdi φ ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k 0 = 0 A M C B N D
121 120 supeq1d φ sup ran k 2 𝑜 A 1 𝑜 B k dist R 1 𝑜 S k C 1 𝑜 D k 0 * < = sup 0 A M C B N D * <
122 0xr 0 *
123 122 a1i φ 0 *
124 123 snssd φ 0 *
125 xmetcl M ∞Met X A X C X A M C *
126 9 11 13 125 syl3anc φ A M C *
127 xmetcl N ∞Met Y B Y D Y B N D *
128 10 12 14 127 syl3anc φ B N D *
129 126 128 prssd φ A M C B N D *
130 xrltso < Or *
131 supsn < Or * 0 * sup 0 * < = 0
132 130 122 131 mp2an sup 0 * < = 0
133 supxrcl A M C B N D * sup A M C B N D * < *
134 129 133 syl φ sup A M C B N D * < *
135 xmetge0 M ∞Met X A X C X 0 A M C
136 9 11 13 135 syl3anc φ 0 A M C
137 ovex A M C V
138 137 prid1 A M C A M C B N D
139 supxrub A M C B N D * A M C A M C B N D A M C sup A M C B N D * <
140 129 138 139 sylancl φ A M C sup A M C B N D * <
141 123 126 134 136 140 xrletrd φ 0 sup A M C B N D * <
142 132 141 eqbrtrid φ sup 0 * < sup A M C B N D * <
143 supxrun 0 * A M C B N D * sup 0 * < sup A M C B N D * < sup 0 A M C B N D * < = sup A M C B N D * <
144 124 129 142 143 syl3anc φ sup 0 A M C B N D * < = sup A M C B N D * <
145 66 121 144 3eqtrd φ A 1 𝑜 B dist Scalar R 𝑠 R 1 𝑜 S C 1 𝑜 D = sup A M C B N D * <
146 49 56 145 3eqtr3d φ A B P C D = sup A M C B N D * <