# Metamath Proof Explorer

## Theorem rrxsphere

Description: The sphere with center M and radius R in a generalized real Euclidean space of finite dimension. Remark: this theorem holds also for the degenerate case R < 0 (negative radius): in this case, ( M S R ) is empty. (Contributed by AV, 5-Feb-2023)

Ref Expression
Hypotheses rrxspheres.e ${⊢}{E}={{I}}^{}$
rrxspheres.p ${⊢}{P}={ℝ}^{{I}}$
rrxspheres.d ${⊢}{D}=\mathrm{dist}\left({E}\right)$
rrxspheres.s ${⊢}{S}=Sphere\left({E}\right)$
Assertion rrxsphere ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$

### Proof

Step Hyp Ref Expression
1 rrxspheres.e ${⊢}{E}={{I}}^{}$
2 rrxspheres.p ${⊢}{P}={ℝ}^{{I}}$
3 rrxspheres.d ${⊢}{D}=\mathrm{dist}\left({E}\right)$
4 rrxspheres.s ${⊢}{S}=Sphere\left({E}\right)$
5 1 fvexi ${⊢}{E}\in \mathrm{V}$
6 id ${⊢}{I}\in \mathrm{Fin}\to {I}\in \mathrm{Fin}$
7 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
8 6 1 7 rrxbasefi ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{{E}}={ℝ}^{{I}}$
9 8 2 syl6reqr ${⊢}{I}\in \mathrm{Fin}\to {P}={\mathrm{Base}}_{{E}}$
10 9 eleq2d ${⊢}{I}\in \mathrm{Fin}\to \left({M}\in {P}↔{M}\in {\mathrm{Base}}_{{E}}\right)$
11 10 biimpa ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\right)\to {M}\in {\mathrm{Base}}_{{E}}$
12 11 3adant3 ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}\in {\mathrm{Base}}_{{E}}$
13 12 adantl ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to {M}\in {\mathrm{Base}}_{{E}}$
14 rexr ${⊢}{R}\in ℝ\to {R}\in {ℝ}^{*}$
15 14 3ad2ant3 ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {R}\in {ℝ}^{*}$
16 15 anim2i ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to \left(0\le {R}\wedge {R}\in {ℝ}^{*}\right)$
17 16 ancomd ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to \left({R}\in {ℝ}^{*}\wedge 0\le {R}\right)$
18 elxrge0 ${⊢}{R}\in \left[0,\mathrm{+\infty }\right]↔\left({R}\in {ℝ}^{*}\wedge 0\le {R}\right)$
19 17 18 sylibr ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to {R}\in \left[0,\mathrm{+\infty }\right]$
20 7 4 3 sphere ${⊢}\left({E}\in \mathrm{V}\wedge {M}\in {\mathrm{Base}}_{{E}}\wedge {R}\in \left[0,\mathrm{+\infty }\right]\right)\to {M}{S}{R}=\left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{M}={R}\right\}$
21 5 13 19 20 mp3an2i ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to {M}{S}{R}=\left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{M}={R}\right\}$
22 simp1 ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {I}\in \mathrm{Fin}$
23 22 1 7 rrxbasefi ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {\mathrm{Base}}_{{E}}={ℝ}^{{I}}$
24 23 2 syl6eqr ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {\mathrm{Base}}_{{E}}={P}$
25 24 adantl ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to {\mathrm{Base}}_{{E}}={P}$
26 25 rabeqdv ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to \left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{M}={R}\right\}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$
27 21 26 eqtrd ${⊢}\left(0\le {R}\wedge \left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$
28 27 ex ${⊢}0\le {R}\to \left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}\right)$
29 7 4 3 spheres ${⊢}{E}\in \mathrm{V}\to {S}=\left({x}\in {\mathrm{Base}}_{{E}},{r}\in \left[0,\mathrm{+\infty }\right]⟼\left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{x}={r}\right\}\right)$
30 5 29 ax-mp ${⊢}{S}=\left({x}\in {\mathrm{Base}}_{{E}},{r}\in \left[0,\mathrm{+\infty }\right]⟼\left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{x}={r}\right\}\right)$
31 fvex ${⊢}{\mathrm{Base}}_{{E}}\in \mathrm{V}$
32 31 rabex ${⊢}\left\{{p}\in {\mathrm{Base}}_{{E}}|{p}{D}{x}={r}\right\}\in \mathrm{V}$
33 30 32 dmmpo ${⊢}\mathrm{dom}{S}={\mathrm{Base}}_{{E}}×\left[0,\mathrm{+\infty }\right]$
34 0xr ${⊢}0\in {ℝ}^{*}$
35 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
36 34 35 pm3.2i ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)$
37 elicc1 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({R}\in \left[0,\mathrm{+\infty }\right]↔\left({R}\in {ℝ}^{*}\wedge 0\le {R}\wedge {R}\le \mathrm{+\infty }\right)\right)$
38 36 37 mp1i ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to \left({R}\in \left[0,\mathrm{+\infty }\right]↔\left({R}\in {ℝ}^{*}\wedge 0\le {R}\wedge {R}\le \mathrm{+\infty }\right)\right)$
39 simp2 ${⊢}\left({R}\in {ℝ}^{*}\wedge 0\le {R}\wedge {R}\le \mathrm{+\infty }\right)\to 0\le {R}$
40 38 39 syl6bi ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to \left({R}\in \left[0,\mathrm{+\infty }\right]\to 0\le {R}\right)$
41 40 con3d ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to \left(¬0\le {R}\to ¬{R}\in \left[0,\mathrm{+\infty }\right]\right)$
42 41 imp ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to ¬{R}\in \left[0,\mathrm{+\infty }\right]$
43 42 intnand ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to ¬\left({M}\in {\mathrm{Base}}_{{E}}\wedge {R}\in \left[0,\mathrm{+\infty }\right]\right)$
44 ndmovg ${⊢}\left(\mathrm{dom}{S}={\mathrm{Base}}_{{E}}×\left[0,\mathrm{+\infty }\right]\wedge ¬\left({M}\in {\mathrm{Base}}_{{E}}\wedge {R}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {M}{S}{R}=\varnothing$
45 33 43 44 sylancr ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to {M}{S}{R}=\varnothing$
46 1 fveq2i ${⊢}\mathrm{dist}\left({E}\right)=\mathrm{dist}\left({{I}}^{}\right)$
47 3 46 eqtri ${⊢}{D}=\mathrm{dist}\left({{I}}^{}\right)$
48 47 rrxmetfi ${⊢}{I}\in \mathrm{Fin}\to {D}\in \mathrm{Met}\left({ℝ}^{{I}}\right)$
49 48 3ad2ant1 ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {D}\in \mathrm{Met}\left({ℝ}^{{I}}\right)$
50 49 adantr ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to {D}\in \mathrm{Met}\left({ℝ}^{{I}}\right)$
51 2 fveq2i ${⊢}\mathrm{Met}\left({P}\right)=\mathrm{Met}\left({ℝ}^{{I}}\right)$
52 50 51 eleqtrrdi ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to {D}\in \mathrm{Met}\left({P}\right)$
53 simpr ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to {p}\in {P}$
54 simp2 ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}\in {P}$
55 54 adantr ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to {M}\in {P}$
56 metge0 ${⊢}\left({D}\in \mathrm{Met}\left({P}\right)\wedge {p}\in {P}\wedge {M}\in {P}\right)\to 0\le {p}{D}{M}$
57 52 53 55 56 syl3anc ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to 0\le {p}{D}{M}$
58 breq2 ${⊢}{p}{D}{M}={R}\to \left(0\le {p}{D}{M}↔0\le {R}\right)$
59 57 58 syl5ibcom ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to \left({p}{D}{M}={R}\to 0\le {R}\right)$
60 59 con3d ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge {p}\in {P}\right)\to \left(¬0\le {R}\to ¬{p}{D}{M}={R}\right)$
61 60 impancom ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to \left({p}\in {P}\to ¬{p}{D}{M}={R}\right)$
62 61 imp ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\wedge {p}\in {P}\right)\to ¬{p}{D}{M}={R}$
63 62 ralrimiva ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to \forall {p}\in {P}\phantom{\rule{.4em}{0ex}}¬{p}{D}{M}={R}$
64 eqcom ${⊢}\varnothing =\left\{{p}\in {P}|{p}{D}{M}={R}\right\}↔\left\{{p}\in {P}|{p}{D}{M}={R}\right\}=\varnothing$
65 rabeq0 ${⊢}\left\{{p}\in {P}|{p}{D}{M}={R}\right\}=\varnothing ↔\forall {p}\in {P}\phantom{\rule{.4em}{0ex}}¬{p}{D}{M}={R}$
66 64 65 bitri ${⊢}\varnothing =\left\{{p}\in {P}|{p}{D}{M}={R}\right\}↔\forall {p}\in {P}\phantom{\rule{.4em}{0ex}}¬{p}{D}{M}={R}$
67 63 66 sylibr ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to \varnothing =\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$
68 45 67 eqtrd ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\wedge ¬0\le {R}\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$
69 68 expcom ${⊢}¬0\le {R}\to \left(\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}\right)$
70 28 69 pm2.61i ${⊢}\left({I}\in \mathrm{Fin}\wedge {M}\in {P}\wedge {R}\in ℝ\right)\to {M}{S}{R}=\left\{{p}\in {P}|{p}{D}{M}={R}\right\}$