Theorem imasf1obl

Description: The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	imasf1obl.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasf1obl.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasf1obl.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
	imasf1obl.r	$$⊢\phi \to R\in Z$$
	imasf1obl.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
	imasf1obl.d	$$⊢D=\mathrm{dist}\left(U\right)$$
	imasf1obl.m	$$⊢\phi \to E\in \mathrm{\infty Met}\left(V\right)$$
	imasf1obl.x	$$⊢\phi \to P\in V$$
	imasf1obl.s	$$⊢\phi \to S\in {ℝ}^{*}$$
Assertion	imasf1obl	$$⊢\phi \to F\left(P\right)\mathrm{ball}\left(D\right)S=F\left[P\mathrm{ball}\left(E\right)S\right]$$

Proof

Step	Hyp	Ref	Expression
1		imasf1obl.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasf1obl.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasf1obl.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
4		imasf1obl.r	$$⊢\phi \to R\in Z$$
5		imasf1obl.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
6		imasf1obl.d	$$⊢D=\mathrm{dist}\left(U\right)$$
7		imasf1obl.m	$$⊢\phi \to E\in \mathrm{\infty Met}\left(V\right)$$
8		imasf1obl.x	$$⊢\phi \to P\in V$$
9		imasf1obl.s	$$⊢\phi \to S\in {ℝ}^{*}$$
10		f1ocnvfv2	$$⊢\left(F:V\underset{1-1\; onto}{⟶}B\wedge x\in B\right)\to F\left(F^{-1}\left(x\right)\right)=x$$
11	3 10	sylan	$$⊢\left(\phi \wedge x\in B\right)\to F\left(F^{-1}\left(x\right)\right)=x$$
12	11	oveq2d	$$⊢\left(\phi \wedge x\in B\right)\to F\left(P\right)DF\left(F^{-1}\left(x\right)\right)=F\left(P\right)Dx$$
13	1	adantr	$$⊢\left(\phi \wedge x\in B\right)\to U=F{“}_{𝑠}R$$
14	2	adantr	$$⊢\left(\phi \wedge x\in B\right)\to V={\mathrm{Base}}_R$$
15	3	adantr	$$⊢\left(\phi \wedge x\in B\right)\to F:V\underset{1-1\; onto}{⟶}B$$
16	4	adantr	$$⊢\left(\phi \wedge x\in B\right)\to R\in Z$$
17	7	adantr	$$⊢\left(\phi \wedge x\in B\right)\to E\in \mathrm{\infty Met}\left(V\right)$$
18	8	adantr	$$⊢\left(\phi \wedge x\in B\right)\to P\in V$$
19		f1ocnv	$$⊢F:V\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}V$$
20	3 19	syl	$$⊢\phi \to F^{-1}:B\underset{1-1\; onto}{⟶}V$$
21		f1of	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}V\to F^{-1}:B⟶V$$
22	20 21	syl	$$⊢\phi \to F^{-1}:B⟶V$$
23	22	ffvelcdmda	$$⊢\left(\phi \wedge x\in B\right)\to F^{-1}\left(x\right)\in V$$
24	13 14 15 16 5 6 17 18 23	imasdsf1o	$$⊢\left(\phi \wedge x\in B\right)\to F\left(P\right)DF\left(F^{-1}\left(x\right)\right)=PE{F}^{-1}\left(x\right)$$
25	12 24	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to F\left(P\right)Dx=PE{F}^{-1}\left(x\right)$$
26	25	breq1d	$$⊢\left(\phi \wedge x\in B\right)\to \left(F\left(P\right)Dx<S\leftrightarrow PE{F}^{-1}\left(x\right)<S\right)$$
27	9	adantr	$$⊢\left(\phi \wedge x\in B\right)\to S\in {ℝ}^{*}$$
28		elbl2	$$⊢\left(\left(E\in \mathrm{\infty Met}\left(V\right)\wedge S\in {ℝ}^{*}\right)\wedge \left(P\in V\wedge F^{-1}\left(x\right)\in V\right)\right)\to \left(F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\leftrightarrow PE{F}^{-1}\left(x\right)<S\right)$$
29	17 27 18 23 28	syl22anc	$$⊢\left(\phi \wedge x\in B\right)\to \left(F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\leftrightarrow PE{F}^{-1}\left(x\right)<S\right)$$
30	26 29	bitr4d	$$⊢\left(\phi \wedge x\in B\right)\to \left(F\left(P\right)Dx<S\leftrightarrow F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\right)$$
31	30	pm5.32da	$$⊢\phi \to \left(\left(x\in B\wedge F\left(P\right)Dx<S\right)\leftrightarrow \left(x\in B\wedge F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\right)\right)$$
32	1 2 3 4 5 6 7	imasf1oxmet	$$⊢\phi \to D\in \mathrm{\infty Met}\left(B\right)$$
33		f1of	$$⊢F:V\underset{1-1\; onto}{⟶}B\to F:V⟶B$$
34	3 33	syl	$$⊢\phi \to F:V⟶B$$
35	34 8	ffvelcdmd	$$⊢\phi \to F\left(P\right)\in B$$
36		elbl	$$⊢\left(D\in \mathrm{\infty Met}\left(B\right)\wedge F\left(P\right)\in B\wedge S\in {ℝ}^{*}\right)\to \left(x\in \left(F\left(P\right)\mathrm{ball}\left(D\right)S\right)\leftrightarrow \left(x\in B\wedge F\left(P\right)Dx<S\right)\right)$$
37	32 35 9 36	syl3anc	$$⊢\phi \to \left(x\in \left(F\left(P\right)\mathrm{ball}\left(D\right)S\right)\leftrightarrow \left(x\in B\wedge F\left(P\right)Dx<S\right)\right)$$
38		f1ofn	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}V\to F^{-1}FnB$$
39		elpreima	$$⊢F^{-1}FnB\to \left(x\in {F^{-1}}^{-1}\left[P\mathrm{ball}\left(E\right)S\right]\leftrightarrow \left(x\in B\wedge F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\right)\right)$$
40	20 38 39	3syl	$$⊢\phi \to \left(x\in {F^{-1}}^{-1}\left[P\mathrm{ball}\left(E\right)S\right]\leftrightarrow \left(x\in B\wedge F^{-1}\left(x\right)\in \left(P\mathrm{ball}\left(E\right)S\right)\right)\right)$$
41	31 37 40	3bitr4d	$$⊢\phi \to \left(x\in \left(F\left(P\right)\mathrm{ball}\left(D\right)S\right)\leftrightarrow x\in {F^{-1}}^{-1}\left[P\mathrm{ball}\left(E\right)S\right]\right)$$
42	41	eqrdv	$$⊢\phi \to F\left(P\right)\mathrm{ball}\left(D\right)S={F^{-1}}^{-1}\left[P\mathrm{ball}\left(E\right)S\right]$$
43		imacnvcnv	$$⊢{F^{-1}}^{-1}\left[P\mathrm{ball}\left(E\right)S\right]=F\left[P\mathrm{ball}\left(E\right)S\right]$$
44	42 43	eqtrdi	$$⊢\phi \to F\left(P\right)\mathrm{ball}\left(D\right)S=F\left[P\mathrm{ball}\left(E\right)S\right]$$