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

Metamath Proof Explorer

Theorem imasdsfn

Description: The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015) (Proof shortened 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 )
	Assertion	imasdsfn	\|- ( ph -> D Fn ( B X. B ) )

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		eqid	\|- ( 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) ) = ( 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) )
8		xrltso	\|- < Or RR*
9	8	infex	\|- 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) e. _V
10	7 9	fnmpoi	\|- ( 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) ) Fn ( B X. B )
11	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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) ) )
12	11	fneq1d	\|- ( ph -> ( D Fn ( B X. B ) <-> ( 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) ) Fn ( B X. B ) ) )
13	10 12	mpbiri	\|- ( ph -> D Fn ( B X. B ) )