Metamath Proof Explorer

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 = Base W
spheres.l ⊢ S = Sphere ⁡ W
spheres.d ⊢ D = dist ⁡ W
Assertion sphere ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → X S R = 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 1 2 3 spheres ⊢ W ∈ V → S = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r
5 4 3ad2ant1 ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → S = x ∈ B , r ∈ 0 +∞ ⟼ p ∈ B | p D x = r
6 oveq2 ⊢ x = X → p D x = p D X
7 id ⊢ r = R → r = R
8 6 7 eqeqan12d ⊢ x = X ∧ r = R → p D x = r ↔ p D X = R
9 8 rabbidv ⊢ x = X ∧ r = R → p ∈ B | p D x = r = p ∈ B | p D X = R
10 9 adantl ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ ∧ x = X ∧ r = R → p ∈ B | p D x = r = p ∈ B | p D X = R
11 simp2 ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → X ∈ B
12 simp3 ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → R ∈ 0 +∞
13 1 fvexi ⊢ B ∈ V
14 13 rabex ⊢ p ∈ B | p D X = R ∈ V
15 14 a1i ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → p ∈ B | p D X = R ∈ V
16 5 10 11 12 15 ovmpod ⊢ W ∈ V ∧ X ∈ B ∧ R ∈ 0 +∞ → X S R = p ∈ B | p D X = R