| Step | Hyp | Ref
| Expression |
| 1 | | rrxspheres.e |
. . . . . 6
⊢ 𝐸 = (ℝ^‘𝐼) |
| 2 | 1 | fvexi 6920 |
. . . . 5
⊢ 𝐸 ∈ V |
| 3 | | rrxspheres.p |
. . . . . . . . . 10
⊢ 𝑃 = (ℝ ↑m
𝐼) |
| 4 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 6 | 4, 1, 5 | rrxbasefi 25444 |
. . . . . . . . . 10
⊢ (𝐼 ∈ Fin →
(Base‘𝐸) = (ℝ
↑m 𝐼)) |
| 7 | 3, 6 | eqtr4id 2796 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin → 𝑃 = (Base‘𝐸)) |
| 8 | 7 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝐼 ∈ Fin → (𝑀 ∈ 𝑃 ↔ 𝑀 ∈ (Base‘𝐸))) |
| 9 | 8 | biimpa 476 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃) → 𝑀 ∈ (Base‘𝐸)) |
| 10 | 9 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → 𝑀 ∈ (Base‘𝐸)) |
| 11 | 10 | adantl 481 |
. . . . 5
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → 𝑀 ∈ (Base‘𝐸)) |
| 12 | | rexr 11307 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → 𝑅 ∈
ℝ*) |
| 13 | 12 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → 𝑅 ∈
ℝ*) |
| 14 | 13 | anim2i 617 |
. . . . . . 7
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → (0 ≤ 𝑅 ∧ 𝑅 ∈
ℝ*)) |
| 15 | 14 | ancomd 461 |
. . . . . 6
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅)) |
| 16 | | elxrge0 13497 |
. . . . . 6
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅)) |
| 17 | 15, 16 | sylibr 234 |
. . . . 5
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → 𝑅 ∈ (0[,]+∞)) |
| 18 | | rrxspheres.s |
. . . . . 6
⊢ 𝑆 = (Sphere‘𝐸) |
| 19 | | rrxspheres.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝐸) |
| 20 | 5, 18, 19 | sphere 48668 |
. . . . 5
⊢ ((𝐸 ∈ V ∧ 𝑀 ∈ (Base‘𝐸) ∧ 𝑅 ∈ (0[,]+∞)) → (𝑀𝑆𝑅) = {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 21 | 2, 11, 17, 20 | mp3an2i 1468 |
. . . 4
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → (𝑀𝑆𝑅) = {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 22 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → 𝐼 ∈ Fin) |
| 23 | 22, 1, 5 | rrxbasefi 25444 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (Base‘𝐸) = (ℝ ↑m
𝐼)) |
| 24 | 23, 3 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (Base‘𝐸) = 𝑃) |
| 25 | 24 | adantl 481 |
. . . . 5
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → (Base‘𝐸) = 𝑃) |
| 26 | 25 | rabeqdv 3452 |
. . . 4
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑀) = 𝑅} = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 27 | 21, 26 | eqtrd 2777 |
. . 3
⊢ ((0 ≤
𝑅 ∧ (𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ)) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 28 | 27 | ex 412 |
. 2
⊢ (0 ≤
𝑅 → ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅})) |
| 29 | 5, 18, 19 | spheres 48667 |
. . . . . . 7
⊢ (𝐸 ∈ V → 𝑆 = (𝑥 ∈ (Base‘𝐸), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑥) = 𝑟})) |
| 30 | 2, 29 | ax-mp 5 |
. . . . . 6
⊢ 𝑆 = (𝑥 ∈ (Base‘𝐸), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑥) = 𝑟}) |
| 31 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝐸)
∈ V |
| 32 | 31 | rabex 5339 |
. . . . . 6
⊢ {𝑝 ∈ (Base‘𝐸) ∣ (𝑝𝐷𝑥) = 𝑟} ∈ V |
| 33 | 30, 32 | dmmpo 8096 |
. . . . 5
⊢ dom 𝑆 = ((Base‘𝐸) ×
(0[,]+∞)) |
| 34 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 35 | | pnfxr 11315 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
| 36 | 34, 35 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (0 ∈
ℝ* ∧ +∞ ∈ ℝ*) |
| 37 | | elicc1 13431 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
| 38 | 36, 37 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑅 ∈ (0[,]+∞) ↔ (𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅 ∧ 𝑅 ≤
+∞))) |
| 39 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞) → 0 ≤
𝑅) |
| 40 | 38, 39 | biimtrdi 253 |
. . . . . . . 8
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑅 ∈ (0[,]+∞) → 0 ≤ 𝑅)) |
| 41 | 40 | con3d 152 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (¬ 0 ≤ 𝑅 → ¬ 𝑅 ∈ (0[,]+∞))) |
| 42 | 41 | imp 406 |
. . . . . 6
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → ¬ 𝑅 ∈ (0[,]+∞)) |
| 43 | 42 | intnand 488 |
. . . . 5
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → ¬ (𝑀 ∈ (Base‘𝐸) ∧ 𝑅 ∈ (0[,]+∞))) |
| 44 | | ndmovg 7616 |
. . . . 5
⊢ ((dom
𝑆 = ((Base‘𝐸) × (0[,]+∞)) ∧
¬ (𝑀 ∈
(Base‘𝐸) ∧ 𝑅 ∈ (0[,]+∞))) →
(𝑀𝑆𝑅) = ∅) |
| 45 | 33, 43, 44 | sylancr 587 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → (𝑀𝑆𝑅) = ∅) |
| 46 | 1 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘𝐸) =
(dist‘(ℝ^‘𝐼)) |
| 47 | 19, 46 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ 𝐷 =
(dist‘(ℝ^‘𝐼)) |
| 48 | 47 | rrxmetfi 25446 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ
↑m 𝐼))) |
| 49 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ (Met‘(ℝ
↑m 𝐼))) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐷 ∈ (Met‘(ℝ
↑m 𝐼))) |
| 51 | 3 | fveq2i 6909 |
. . . . . . . . . . . 12
⊢
(Met‘𝑃) =
(Met‘(ℝ ↑m 𝐼)) |
| 52 | 50, 51 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐷 ∈ (Met‘𝑃)) |
| 53 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃) |
| 54 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → 𝑀 ∈ 𝑃) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝑀 ∈ 𝑃) |
| 56 | | metge0 24355 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Met‘𝑃) ∧ 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃) → 0 ≤ (𝑝𝐷𝑀)) |
| 57 | 52, 53, 55, 56 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 0 ≤ (𝑝𝐷𝑀)) |
| 58 | | breq2 5147 |
. . . . . . . . . 10
⊢ ((𝑝𝐷𝑀) = 𝑅 → (0 ≤ (𝑝𝐷𝑀) ↔ 0 ≤ 𝑅)) |
| 59 | 57, 58 | syl5ibcom 245 |
. . . . . . . . 9
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝𝐷𝑀) = 𝑅 → 0 ≤ 𝑅)) |
| 60 | 59 | con3d 152 |
. . . . . . . 8
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (¬ 0 ≤ 𝑅 → ¬ (𝑝𝐷𝑀) = 𝑅)) |
| 61 | 60 | impancom 451 |
. . . . . . 7
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → (𝑝 ∈ 𝑃 → ¬ (𝑝𝐷𝑀) = 𝑅)) |
| 62 | 61 | imp 406 |
. . . . . 6
⊢ ((((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) ∧ 𝑝 ∈ 𝑃) → ¬ (𝑝𝐷𝑀) = 𝑅) |
| 63 | 62 | ralrimiva 3146 |
. . . . 5
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → ∀𝑝 ∈ 𝑃 ¬ (𝑝𝐷𝑀) = 𝑅) |
| 64 | | eqcom 2744 |
. . . . . 6
⊢ (∅
= {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅} ↔ {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅} = ∅) |
| 65 | | rabeq0 4388 |
. . . . . 6
⊢ ({𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅} = ∅ ↔ ∀𝑝 ∈ 𝑃 ¬ (𝑝𝐷𝑀) = 𝑅) |
| 66 | 64, 65 | bitri 275 |
. . . . 5
⊢ (∅
= {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅} ↔ ∀𝑝 ∈ 𝑃 ¬ (𝑝𝐷𝑀) = 𝑅) |
| 67 | 63, 66 | sylibr 234 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → ∅ = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 68 | 45, 67 | eqtrd 2777 |
. . 3
⊢ (((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) ∧ ¬ 0 ≤ 𝑅) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) |
| 69 | 68 | expcom 413 |
. 2
⊢ (¬ 0
≤ 𝑅 → ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅})) |
| 70 | 28, 69 | pm2.61i 182 |
1
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) |