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	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasdsf1o.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasdsf1o.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
	imasdsf1o.r	$$⊢\phi \to R\in Z$$
	imasdsf1o.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
	imasdsf1o.d	$$⊢D=\mathrm{dist}\left(U\right)$$
	imasdsf1o.m	$$⊢\phi \to E\in \mathrm{\infty Met}\left(V\right)$$
	imasdsf1o.x	$$⊢\phi \to X\in V$$
	imasdsf1o.y	$$⊢\phi \to Y\in V$$
Assertion	imasdsf1o	$$⊢\phi \to F\left(X\right)DF\left(Y\right)=XEY$$

Proof

Step	Hyp	Ref	Expression
1		imasdsf1o.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasdsf1o.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasdsf1o.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
4		imasdsf1o.r	$$⊢\phi \to R\in Z$$
5		imasdsf1o.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
6		imasdsf1o.d	$$⊢D=\mathrm{dist}\left(U\right)$$
7		imasdsf1o.m	$$⊢\phi \to E\in \mathrm{\infty Met}\left(V\right)$$
8		imasdsf1o.x	$$⊢\phi \to X\in V$$
9		imasdsf1o.y	$$⊢\phi \to Y\in V$$
10		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
11		eqid	$$⊢\left\{h\in \left({\left(V\times V\right)}^{\left(1\dots n\right)}\right)|\left(F\left(1^{st}\left(h\left(1\right)\right)\right)=F\left(X\right)\wedge F\left(2^{nd}\left(h\left(n\right)\right)\right)=F\left(Y\right)\wedge \forall i\in \left(1\dots n-1\right)F\left(2^{nd}\left(h\left(i\right)\right)\right)=F\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}=\left\{h\in \left({\left(V\times V\right)}^{\left(1\dots n\right)}\right)|\left(F\left(1^{st}\left(h\left(1\right)\right)\right)=F\left(X\right)\wedge F\left(2^{nd}\left(h\left(n\right)\right)\right)=F\left(Y\right)\wedge \forall i\in \left(1\dots n-1\right)F\left(2^{nd}\left(h\left(i\right)\right)\right)=F\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}$$
12		eqid	$$⊢\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times V\right)}^{\left(1\dots n\right)}\right)|\left(F\left(1^{st}\left(h\left(1\right)\right)\right)=F\left(X\right)\wedge F\left(2^{nd}\left(h\left(n\right)\right)\right)=F\left(Y\right)\wedge \forall i\in \left(1\dots n-1\right)F\left(2^{nd}\left(h\left(i\right)\right)\right)=F\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(E\circ g\right)\right)=\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times V\right)}^{\left(1\dots n\right)}\right)|\left(F\left(1^{st}\left(h\left(1\right)\right)\right)=F\left(X\right)\wedge F\left(2^{nd}\left(h\left(n\right)\right)\right)=F\left(Y\right)\wedge \forall i\in \left(1\dots n-1\right)F\left(2^{nd}\left(h\left(i\right)\right)\right)=F\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(E\circ g\right)\right)$$
13	1 2 3 4 5 6 7 8 9 10 11 12	imasdsf1olem	$$⊢\phi \to F\left(X\right)DF\left(Y\right)=XEY$$