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 ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
rrxspheres.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
rrxspheres.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
rrxspheres.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
Assertion rrxsphere ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )

Proof

Step Hyp Ref Expression
1 rrxspheres.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
2 rrxspheres.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3 rrxspheres.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 rrxspheres.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 1 fvexi ⊢ 𝐸 ∈ V
6 id ⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
7 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 6 1 7 rrxbasefi ⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
9 2 8 eqtr4id ⊢ ( 𝐼 ∈ Fin → 𝑃 = ( Base ‘ 𝐸 ) )
10 9 eleq2d ⊢ ( 𝐼 ∈ Fin → ( 𝑀 ∈ 𝑃 ↔ 𝑀 ∈ ( Base ‘ 𝐸 ) ) )
11 10 biimpa ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ) → 𝑀 ∈ ( Base ‘ 𝐸 ) )
12 11 3adant3 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → 𝑀 ∈ ( Base ‘ 𝐸 ) )
13 12 adantl ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → 𝑀 ∈ ( Base ‘ 𝐸 ) )
14 rexr ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℝ* )
15 14 3ad2ant3 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → 𝑅 ∈ ℝ* )
16 15 anim2i ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → ( 0 ≤ 𝑅 ∧ 𝑅 ∈ ℝ* ) )
17 16 ancomd ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) )
18 elxrge0 ⊢ ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) )
19 17 18 sylibr ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → 𝑅 ∈ ( 0 [,] +∞ ) )
20 7 4 3 sphere ⊢ ( ( 𝐸 ∈ V ∧ 𝑀 ∈ ( Base ‘ 𝐸 ) ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
21 5 13 19 20 mp3an2i ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
22 simp1 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → 𝐼 ∈ Fin )
23 22 1 7 rrxbasefi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
24 23 2 eqtr4di ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( Base ‘ 𝐸 ) = 𝑃 )
25 24 adantl ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → ( Base ‘ 𝐸 ) = 𝑃 )
26 25 rabeqdv ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
27 21 26 eqtrd ⊢ ( ( 0 ≤ 𝑅 ∧ ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
28 27 ex ⊢ ( 0 ≤ 𝑅 → ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } ) )
29 7 4 3 spheres ⊢ ( 𝐸 ∈ V → 𝑆 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )
30 5 29 ax-mp ⊢ 𝑆 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } )
31 fvex ⊢ ( Base ‘ 𝐸 ) ∈ V
32 31 rabex ⊢ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ∈ V
33 30 32 dmmpo ⊢ dom 𝑆 = ( ( Base ‘ 𝐸 ) × ( 0 [,] +∞ ) )
34 0xr ⊢ 0 ∈ ℝ*
35 pnfxr ⊢ +∞ ∈ ℝ*
36 34 35 pm3.2i ⊢ ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* )
37 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) )
38 36 37 mp1i ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) )
39 simp2 ⊢ ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) → 0 ≤ 𝑅 )
40 38 39 syl6bi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑅 ) )
41 40 con3d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( ¬ 0 ≤ 𝑅 → ¬ 𝑅 ∈ ( 0 [,] +∞ ) ) )
42 41 imp ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ¬ 𝑅 ∈ ( 0 [,] +∞ ) )
43 42 intnand ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ¬ ( 𝑀 ∈ ( Base ‘ 𝐸 ) ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) )
44 ndmovg ⊢ ( ( dom 𝑆 = ( ( Base ‘ 𝐸 ) × ( 0 [,] +∞ ) ) ∧ ¬ ( 𝑀 ∈ ( Base ‘ 𝐸 ) ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑀 𝑆 𝑅 ) = ∅ )
45 33 43 44 sylancr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ( 𝑀 𝑆 𝑅 ) = ∅ )
46 1 fveq2i ⊢ ( dist ‘ 𝐸 ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
47 3 46 eqtri ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
48 47 rrxmetfi ⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
49 48 3ad2ant1 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
50 49 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
51 2 fveq2i ⊢ ( Met ‘ 𝑃 ) = ( Met ‘ ( ℝ ↑m 𝐼 ) )
52 50 51 eleqtrrdi ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐷 ∈ ( Met ‘ 𝑃 ) )
53 simpr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
54 simp2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → 𝑀 ∈ 𝑃 )
55 54 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝑀 ∈ 𝑃 )
56 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑃 ) ∧ 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃 ) → 0 ≤ ( 𝑝 𝐷 𝑀 ) )
57 52 53 55 56 syl3anc ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( 𝑝 𝐷 𝑀 ) )
58 breq2 ⊢ ( ( 𝑝 𝐷 𝑀 ) = 𝑅 → ( 0 ≤ ( 𝑝 𝐷 𝑀 ) ↔ 0 ≤ 𝑅 ) )
59 57 58 syl5ibcom ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 𝐷 𝑀 ) = 𝑅 → 0 ≤ 𝑅 ) )
60 59 con3d ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ¬ 0 ≤ 𝑅 → ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 ) )
61 60 impancom ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ( 𝑝 ∈ 𝑃 → ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 ) )
62 61 imp ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 )
63 62 ralrimiva ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ∀ 𝑝 ∈ 𝑃 ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 )
64 eqcom ⊢ ( ∅ = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } ↔ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } = ∅ )
65 rabeq0 ⊢ ( { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } = ∅ ↔ ∀ 𝑝 ∈ 𝑃 ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 )
66 64 65 bitri ⊢ ( ∅ = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } ↔ ∀ 𝑝 ∈ 𝑃 ¬ ( 𝑝 𝐷 𝑀 ) = 𝑅 )
67 63 66 sylibr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ∅ = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
68 45 67 eqtrd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) ∧ ¬ 0 ≤ 𝑅 ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )
69 68 expcom ⊢ ( ¬ 0 ≤ 𝑅 → ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } ) )
70 28 69 pm2.61i ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 𝐷 𝑀 ) = 𝑅 } )