Metamath Proof Explorer


Theorem imasdsval2

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
imasds.u T = E V × V
Assertion imasdsval2 φ X D Y = sup n ran g S 𝑠 * T 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 imasds.u T = E V × V
11 1 2 3 4 5 6 7 8 9 imasdsval φ X D Y = sup n ran g S 𝑠 * E g * <
12 10 coeq1i T g = E V × V g
13 9 ssrab3 S V × V 1 n
14 13 sseli g S g V × V 1 n
15 elmapi g V × V 1 n g : 1 n V × V
16 frn g : 1 n V × V ran g V × V
17 cores ran g V × V E V × V g = E g
18 14 15 16 17 4syl g S E V × V g = E g
19 12 18 eqtrid g S T g = E g
20 19 oveq2d g S 𝑠 * T g = 𝑠 * E g
21 20 mpteq2ia g S 𝑠 * T g = g S 𝑠 * E g
22 21 rneqi ran g S 𝑠 * T g = ran g S 𝑠 * E g
23 22 a1i n ran g S 𝑠 * T g = ran g S 𝑠 * E g
24 23 iuneq2i n ran g S 𝑠 * T g = n ran g S 𝑠 * E g
25 24 infeq1i sup n ran g S 𝑠 * T g * < = sup n ran g S 𝑠 * E g * <
26 11 25 eqtr4di φ X D Y = sup n ran g S 𝑠 * T g * <