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