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
|- ( 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 ) ) ) ) ) }
Assertion imasdsval
|- ( ph -> ( X D Y ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E 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 1 2 3 4 5 6 imasds
 |-  ( ph -> D = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { 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 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) ) )
11 simplrl
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> x = X )
12 11 eqeq2d
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x <-> ( F ` ( 1st ` ( h ` 1 ) ) ) = X ) )
13 simplrr
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> y = Y )
14 13 eqeq2d
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = y <-> ( F ` ( 2nd ` ( h ` n ) ) ) = Y ) )
15 12 14 3anbi12d
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> ( ( ( 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 ) ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
16 15 rabbidv
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> { 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 ) ) ) ) ) } = { 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 ) ) ) ) ) } )
17 16 9 eqtr4di
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> { 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 ) ) ) ) ) } = S )
18 17 mpteq1d
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> ( g e. { 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 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
19 18 rneqd
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ n e. NN ) -> ran ( g e. { 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 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) = ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
20 19 iuneq2dv
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> U_ n e. NN ran ( g e. { 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 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) = U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
21 20 infeq1d
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> inf ( U_ n e. NN ran ( g e. { 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 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) )
22 xrltso
 |-  < Or RR*
23 22 infex
 |-  inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) e. _V
24 23 a1i
 |-  ( ph -> inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) e. _V )
25 10 21 7 8 24 ovmpod
 |-  ( ph -> ( X D Y ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) )