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 e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> ( X S R ) = { p e. 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 e. V -> S = ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) )
5	4	3ad2ant1	|- ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> S = ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. 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 e. B | ( p D x ) = r } = { p e. B | ( p D X ) = R } )
10	9	adantl	|- ( ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) /\ ( x = X /\ r = R ) ) -> { p e. B | ( p D x ) = r } = { p e. B | ( p D X ) = R } )
11		simp2	|- ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> X e. B )
12		simp3	|- ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> R e. ( 0 [,] +oo ) )
13	1	fvexi	|- B e. _V
14	13	rabex	|- { p e. B | ( p D X ) = R } e. _V
15	14	a1i	|- ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> { p e. B | ( p D X ) = R } e. _V )
16	5 10 11 12 15	ovmpod	|- ( ( W e. V /\ X e. B /\ R e. ( 0 [,] +oo ) ) -> ( X S R ) = { p e. B | ( p D X ) = R } )