This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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