Metamath Proof Explorer


Theorem spheres

Description: The spheres for given centers and radii 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=BaseW
spheres.l S=SphereW
spheres.d D=distW
Assertion spheres WVS=xB,r0+∞pB|pDx=r

Proof

Step Hyp Ref Expression
1 spheres.b B=BaseW
2 spheres.l S=SphereW
3 spheres.d D=distW
4 2 a1i WVS=SphereW
5 df-sph Sphere=wVxBasew,r0+∞pBasew|pdistwx=r
6 fveq2 w=WBasew=BaseW
7 1 eqcomi BaseW=B
8 7 a1i w=WBaseW=B
9 6 8 eqtrd w=WBasew=B
10 eqidd w=W0+∞=0+∞
11 fveq2 w=Wdistw=distW
12 3 eqcomi distW=D
13 12 a1i w=WdistW=D
14 11 13 eqtrd w=Wdistw=D
15 14 oveqd w=Wpdistwx=pDx
16 15 eqeq1d w=Wpdistwx=rpDx=r
17 9 16 rabeqbidv w=WpBasew|pdistwx=r=pB|pDx=r
18 9 10 17 mpoeq123dv w=WxBasew,r0+∞pBasew|pdistwx=r=xB,r0+∞pB|pDx=r
19 elex WVWV
20 fvex BaseWV
21 1 20 eqeltri BV
22 ovex 0+∞V
23 21 22 mpoex xB,r0+∞pB|pDx=rV
24 23 a1i WVxB,r0+∞pB|pDx=rV
25 5 18 19 24 fvmptd3 WVSphereW=xB,r0+∞pB|pDx=r
26 4 25 eqtrd WVS=xB,r0+∞pB|pDx=r