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 e. V -> S = ( x e. B , r e. ( 0 [,] +oo ) |-> { 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 2 a1i 
 |-  ( W e. V -> S = ( Sphere ` W ) )
5 df-sph 
 |-  Sphere = ( w e. _V |-> ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( 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 [,] +oo ) = ( 0 [,] +oo ) )
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 e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } = { p e. B | ( p D x ) = r } )
18 9 10 17 mpoeq123dv 
 |-  ( w = W -> ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } ) = ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) )
19 elex 
 |-  ( W e. V -> W e. _V )
20 fvex 
 |-  ( Base ` W ) e. _V
21 1 20 eqeltri 
 |-  B e. _V
22 ovex 
 |-  ( 0 [,] +oo ) e. _V
23 21 22 mpoex 
 |-  ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) e. _V
24 23 a1i 
 |-  ( W e. V -> ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) e. _V )
25 5 18 19 24 fvmptd3 
 |-  ( W e. V -> ( Sphere ` W ) = ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) )
26 4 25 eqtrd 
 |-  ( W e. V -> S = ( x e. B , r e. ( 0 [,] +oo ) |-> { p e. B | ( p D x ) = r } ) )