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