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 = Base W
spheres.l ⊢ S = Sphere ⁡ W
spheres.d ⊢ D = dist ⁡ W
Assertion spheres ⊢ W ∈ V → S = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r

Proof

Step Hyp Ref Expression
1 spheres.b ⊢ B = Base W
2 spheres.l ⊢ S = Sphere ⁡ W
3 spheres.d ⊢ D = dist ⁡ W
4 2 a1i ⊢ W ∈ V → S = Sphere ⁡ W
5 df-sph ⊢ Sphere = w ∈ V ⟼ x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r
6 fveq2 ⊢ w = W → Base w = Base W
7 1 eqcomi ⊢ Base W = B
8 7 a1i ⊢ w = W → Base W = B
9 6 8 eqtrd ⊢ w = W → Base w = B
10 eqidd ⊢ w = W → 0 +∞ = 0 +∞
11 fveq2 ⊢ w = W → dist ⁡ w = dist ⁡ W
12 3 eqcomi ⊢ dist ⁡ W = D
13 12 a1i ⊢ w = W → dist ⁡ W = D
14 11 13 eqtrd ⊢ w = W → dist ⁡ w = D
15 14 oveqd ⊢ w = W → p dist ⁡ w x = p D x
16 15 eqeq1d ⊢ w = W → p dist ⁡ w x = r ↔ p D x = r
17 9 16 rabeqbidv ⊢ w = W → p ∈ Base w | p dist ⁡ w x = r = p ∈ B | p D x = r
18 9 10 17 mpoeq123dv ⊢ w = W → x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r
19 elex ⊢ W ∈ V → W ∈ V
20 fvex ⊢ Base W ∈ V
21 1 20 eqeltri ⊢ B ∈ V
22 ovex ⊢ 0 +∞ ∈ V
23 21 22 mpoex ⊢ x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r ∈ V
24 23 a1i ⊢ W ∈ V → x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r ∈ V
25 5 18 19 24 fvmptd3 ⊢ W ∈ V → Sphere ⁡ W = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r
26 4 25 eqtrd ⊢ W ∈ V → S = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r