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 \|-> ( RRs 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 ) ) ) ) ) } \|-> ( RRs 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) = ( g e. S \|-> ( RRs 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) = ran ( g e. S \|-> ( RRs 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) = U_ n e. NN ran ( g e. S \|-> ( RRs 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 ) ) ) ) ) } \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) = inf ( U_ n e. NN ran ( g e. S \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) )
22		xrltso	\|- < Or RR*
23	22	infex	\|- inf ( U_ n e. NN ran ( g e. S \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) e. _V
24	23	a1i	\|- ( ph -> inf ( U_ n e. NN ran ( g e. S \|-> ( RRs 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 \|-> ( RRs gsum ( E o. g ) ) ) , RR , < ) )

Metamath Proof Explorer

Theorem imasdsval

Proof