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
|- ( ph -> U = ( F "s R ) )
imasbas.v
|- ( ph -> V = ( Base ` R ) )
imasbas.f
|- ( ph -> F : V -onto-> B )
imasbas.r
|- ( ph -> R e. Z )
imasds.e
|- E = ( dist ` R )
imasds.d
|- D = ( dist ` U )
imasdsval.x
|- ( ph -> X e. B )
imasdsval.y
|- ( ph -> Y e. B )
imasdsval.s
|- S = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = X /\ ( F ` ( 2nd ` ( h ` n ) ) ) = Y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }
imasds.u
|- T = ( E |` ( V X. V ) )
Assertion imasdsval2
|- ( ph -> ( X D Y ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 imasbas.u
 |-  ( ph -> U = ( F "s R ) )
2 imasbas.v
 |-  ( ph -> V = ( Base ` R ) )
3 imasbas.f
 |-  ( ph -> F : V -onto-> B )
4 imasbas.r
 |-  ( ph -> R e. Z )
5 imasds.e
 |-  E = ( dist ` R )
6 imasds.d
 |-  D = ( dist ` U )
7 imasdsval.x
 |-  ( ph -> X e. B )
8 imasdsval.y
 |-  ( ph -> Y e. B )
9 imasdsval.s
 |-  S = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = X /\ ( F ` ( 2nd ` ( h ` n ) ) ) = Y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }
10 imasds.u
 |-  T = ( E |` ( V X. V ) )
11 1 2 3 4 5 6 7 8 9 imasdsval
 |-  ( ph -> ( X D Y ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) )
12 10 coeq1i
 |-  ( T o. g ) = ( ( E |` ( V X. V ) ) o. g )
13 9 ssrab3
 |-  S C_ ( ( V X. V ) ^m ( 1 ... n ) )
14 13 sseli
 |-  ( g e. S -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
15 elmapi
 |-  ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
16 frn
 |-  ( g : ( 1 ... n ) --> ( V X. V ) -> ran g C_ ( V X. V ) )
17 cores
 |-  ( ran g C_ ( V X. V ) -> ( ( E |` ( V X. V ) ) o. g ) = ( E o. g ) )
18 14 15 16 17 4syl
 |-  ( g e. S -> ( ( E |` ( V X. V ) ) o. g ) = ( E o. g ) )
19 12 18 eqtrid
 |-  ( g e. S -> ( T o. g ) = ( E o. g ) )
20 19 oveq2d
 |-  ( g e. S -> ( RR*s gsum ( T o. g ) ) = ( RR*s gsum ( E o. g ) ) )
21 20 mpteq2ia
 |-  ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) = ( g e. S |-> ( RR*s gsum ( E o. g ) ) )
22 21 rneqi
 |-  ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) = ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) )
23 22 a1i
 |-  ( n e. NN -> ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) = ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
24 23 iuneq2i
 |-  U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) = U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) )
25 24 infeq1i
 |-  inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) , RR* , < ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < )
26 11 25 eqtr4di
 |-  ( ph -> ( X D Y ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( T o. g ) ) ) , RR* , < ) )