Theorem sphere

Description: A sphere with center X and radius R in a metric space (or any extensible structure having a base set and a distance function). (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	spheres.b	$$⊢B={\mathrm{Base}}_W$$
	spheres.l	$$⊢S=Sphere\left(W\right)$$
	spheres.d	$$⊢D=\mathrm{dist}\left(W\right)$$
Assertion	sphere	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to XSR=\left\{p\in B|pDX=R\right\}$$

Proof

Step	Hyp	Ref	Expression
1		spheres.b	$$⊢B={\mathrm{Base}}_W$$
2		spheres.l	$$⊢S=Sphere\left(W\right)$$
3		spheres.d	$$⊢D=\mathrm{dist}\left(W\right)$$
4	1 2 3	spheres	$$⊢W\in V\to S=\left(x\in B,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in B|pDx=r\right\}\right)$$
5	4	3ad2ant1	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to S=\left(x\in B,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in B|pDx=r\right\}\right)$$
6		oveq2	$$⊢x=X\to pDx=pDX$$
7		id	$$⊢r=R\to r=R$$
8	6 7	eqeqan12d	$$⊢\left(x=X\wedge r=R\right)\to \left(pDx=r\leftrightarrow pDX=R\right)$$
9	8	rabbidv	$$⊢\left(x=X\wedge r=R\right)\to \left\{p\in B|pDx=r\right\}=\left\{p\in B|pDX=R\right\}$$
10	9	adantl	$$⊢\left(\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\wedge \left(x=X\wedge r=R\right)\right)\to \left\{p\in B|pDx=r\right\}=\left\{p\in B|pDX=R\right\}$$
11		simp2	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to X\in B$$
12		simp3	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to R\in \left[0,\mathrm{+\infty }\right]$$
13	1	fvexi	$$⊢B\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{p\in B|pDX=R\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to \left\{p\in B|pDX=R\right\}\in \mathrm{V}$$
16	5 10 11 12 15	ovmpod	$$⊢\left(W\in V\wedge X\in B\wedge R\in \left[0,\mathrm{+\infty }\right]\right)\to XSR=\left\{p\in B|pDX=R\right\}$$