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

Metamath Proof Explorer

Theorem imasdsf1o

Description: The distance function is transferred across an image structure under a bijection. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasdsf1o.u 
|- ( ph -> U = ( F "s R ) )
imasdsf1o.v 
|- ( ph -> V = ( Base ` R ) )
imasdsf1o.f 
|- ( ph -> F : V -1-1-onto-> B )
imasdsf1o.r 
|- ( ph -> R e. Z )
imasdsf1o.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
imasdsf1o.d 
|- D = ( dist ` U )
imasdsf1o.m 
|- ( ph -> E e. ( *Met ` V ) )
imasdsf1o.x 
|- ( ph -> X e. V )
imasdsf1o.y 
|- ( ph -> Y e. V )
Assertion imasdsf1o 
|- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )

Proof

Step Hyp Ref Expression
1 imasdsf1o.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasdsf1o.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasdsf1o.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasdsf1o.r 
 |-  ( ph -> R e. Z )
5 imasdsf1o.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
6 imasdsf1o.d 
 |-  D = ( dist ` U )
7 imasdsf1o.m 
 |-  ( ph -> E e. ( *Met ` V ) )
8 imasdsf1o.x 
 |-  ( ph -> X e. V )
9 imasdsf1o.y 
 |-  ( ph -> Y e. V )
10 eqid 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
11 eqid 
 |-  { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` 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 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }
12 eqid 
 |-  U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` 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. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 imasdsf1olem 
 |-  ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )