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 = dist E
rrxspheres.s S = Sphere E
Assertion rrxsphere I Fin M P R M S R = p P | p D M = R

Proof

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