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* , < ) )