Metamath Proof Explorer


Theorem imasdsval

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasbas.u φ U = F 𝑠 R
imasbas.v φ V = Base R
imasbas.f φ F : V onto B
imasbas.r φ R Z
imasds.e E = dist R
imasds.d D = dist U
imasdsval.x φ X B
imasdsval.y φ Y B
imasdsval.s S = h V × V 1 n | F 1 st h 1 = X F 2 nd h n = Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
Assertion imasdsval φ X D Y = sup n ran g S 𝑠 * E g * <

Proof

Step Hyp Ref Expression
1 imasbas.u φ U = F 𝑠 R
2 imasbas.v φ V = Base R
3 imasbas.f φ F : V onto B
4 imasbas.r φ R Z
5 imasds.e E = dist R
6 imasds.d D = dist U
7 imasdsval.x φ X B
8 imasdsval.y φ Y B
9 imasdsval.s S = h V × V 1 n | F 1 st h 1 = X F 2 nd h n = Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
10 1 2 3 4 5 6 imasds φ D = x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * <
11 simplrl φ x = X y = Y n x = X
12 11 eqeq2d φ x = X y = Y n F 1 st h 1 = x F 1 st h 1 = X
13 simplrr φ x = X y = Y n y = Y
14 13 eqeq2d φ x = X y = Y n F 2 nd h n = y F 2 nd h n = Y
15 12 14 3anbi12d φ x = X y = Y n F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 F 1 st h 1 = X F 2 nd h n = Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
16 15 rabbidv φ x = X y = Y n h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 = h V × V 1 n | F 1 st h 1 = X F 2 nd h n = Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
17 16 9 eqtr4di φ x = X y = Y n h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 = S
18 17 mpteq1d φ x = X y = Y n g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g = g S 𝑠 * E g
19 18 rneqd φ x = X y = Y n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g = ran g S 𝑠 * E g
20 19 iuneq2dv φ x = X y = Y n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g = n ran g S 𝑠 * E g
21 20 infeq1d φ x = X y = Y sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * < = sup n ran g S 𝑠 * E g * <
22 xrltso < Or *
23 22 infex sup n ran g S 𝑠 * E g * < V
24 23 a1i φ sup n ran g S 𝑠 * E g * < V
25 10 21 7 8 24 ovmpod φ X D Y = sup n ran g S 𝑠 * E g * <