Step | Hyp | Ref
| Expression |
1 | | totbndbnd 35874 |
. 2
⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴)) |
2 | | bndmet 35866 |
. . . . 5
⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴)) |
3 | | 0totbnd 35858 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴))) |
4 | 2, 3 | syl5ibr 245 |
. . . 4
⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
6 | | n0 4277 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔
∃𝑎 𝑎 ∈ 𝐴) |
7 | | simprr 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴)) |
8 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
9 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
10 | | prdsbnd.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Base‘(𝑅‘𝑥)) |
11 | | prdsbnd.e |
. . . . . . . . . . . 12
⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) |
12 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
13 | | prdsbnd.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
14 | | prdsbnd.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ Fin) |
15 | | fvexd 6771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
16 | | prdsbnd2.e |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
17 | 8, 9, 10, 11, 12, 13, 14, 15, 16 | prdsmet 23431 |
. . . . . . . . . . 11
⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
18 | | prdsbnd.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝑌) |
19 | | prdsbnd.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 = (𝑆Xs𝑅) |
20 | | prdsbnd.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 Fn 𝐼) |
21 | | dffn5 6810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
23 | 22 | oveq2d 7271 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
24 | 19, 23 | syl5eq 2791 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
25 | 24 | fveq2d 6760 |
. . . . . . . . . . . 12
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
26 | 18, 25 | syl5eq 2791 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
27 | | prdsbnd.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑌) |
28 | 24 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
29 | 27, 28 | syl5eq 2791 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
30 | 29 | fveq2d 6760 |
. . . . . . . . . . 11
⊢ (𝜑 → (Met‘𝐵) =
(Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
31 | 17, 26, 30 | 3eltr4d 2854 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵)) |
33 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴)) |
34 | | prdsbnd2.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) |
35 | 34 | bnd2lem 35876 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵) |
36 | 31, 33, 35 | syl2an 595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵) |
37 | | simprl 767 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴) |
38 | 36, 37 | sseldd 3918 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵) |
39 | 34 | ssbnd 35873 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
40 | 32, 38, 39 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
41 | 7, 40 | mpbid 231 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
42 | | simprr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
43 | | xpss12 5595 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
44 | 42, 42, 43 | syl2anc 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
45 | 44 | resabs1d 5911 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴))) |
46 | 45, 34 | eqtr4di 2797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶) |
47 | | simpll 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑) |
48 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵) |
49 | | simprl 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ) |
50 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴) |
51 | 42, 50 | sseldd 3918 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟)) |
52 | 51 | ne0d 4266 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅) |
53 | 31 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵)) |
54 | | metxmet 23395 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵)) |
56 | 49 | rexrd 10956 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ*) |
57 | | xbln0 23475 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
58 | 55, 48, 56, 57 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
59 | 52, 58 | mpbid 231 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟) |
60 | 49, 59 | elrpd 12698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ+) |
61 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) |
62 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) |
63 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘((𝑦
∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) |
64 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
((dist‘((𝑦
∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) |
65 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) |
66 | 13 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑆 ∈ 𝑊) |
67 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) |
68 | | ovex 7288 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V |
69 | | fveq2 6756 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
70 | | 2fveq3 6761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥))) |
71 | | 2fveq3 6761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥))) |
72 | 71, 10 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉) |
73 | 72 | sqxpeqd 5612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉)) |
74 | 70, 73 | reseq12d 5881 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))) |
75 | 74, 11 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸) |
76 | 75 | fveq2d 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸)) |
77 | | fveq2 6756 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥)) |
78 | | eqidd 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟) |
79 | 76, 77, 78 | oveq123d 7276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
80 | 69, 79 | oveq12d 7273 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
81 | 80 | cbvmptv 5183 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
82 | 68, 81 | fnmpti 6560 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼 |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼) |
84 | 16 | adantlr 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
85 | | metxmet 23395 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
87 | 15 | ralrimiva 3107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
89 | | simprl 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ 𝐵) |
90 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
91 | 89, 90 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
92 | 8, 9, 66, 67, 88, 10, 91 | prdsbascl 17111 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉) |
93 | 92 | r19.21bi 3132 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉) |
94 | | simplrr 774 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ+) |
95 | 94 | rpred 12701 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ) |
96 | | blbnd 35872 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
97 | 86, 93, 95, 96 | syl3anc 1369 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
98 | | ovex 7288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V |
99 | | xpeq12 5605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
100 | 99 | anidms 566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
101 | 100 | reseq2d 5880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
102 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
103 | 101, 102 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
104 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
105 | 101, 104 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
106 | 103, 105 | bibi12d 345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
107 | 106 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) |
108 | | prdsbnd2.m |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) |
109 | 98, 107, 108 | vtocl 3488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
110 | 109 | adantlr 711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
111 | 97, 110 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
112 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) |
113 | 80, 112, 68 | fvmpt 6857 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
114 | 113 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
115 | 114 | fveq2d 6760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
116 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
117 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥)) |
118 | 116, 117 | ressds 17039 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
119 | 98, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
120 | 115, 119 | eqtr4di 2797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥))) |
121 | 114 | fveq2d 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
122 | | rpxr 12668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
123 | 122 | ad2antll 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
124 | 123 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ*) |
125 | | blssm 23479 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
126 | 86, 93, 124, 125 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
127 | 116, 10 | ressbas2 16875 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
129 | 121, 128 | eqtr4d 2781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
130 | 129 | sqxpeqd 5612 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
131 | 120, 130 | reseq12d 5881 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
132 | 11 | reseq1i 5876 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
133 | | xpss12 5595 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
134 | 126, 126,
133 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
135 | 134 | resabs1d 5911 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
136 | 132, 135 | syl5eq 2791 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
137 | 131, 136 | eqtr4d 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
138 | 129 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
139 | 111, 137,
138 | 3eltr4d 2854 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) ∈ (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) |
140 | 61, 62, 63, 64, 65, 66, 67, 83, 139 | prdstotbnd 35879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))))) |
141 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
142 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
143 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
144 | 81 | oveq2i 7266 |
. . . . . . . . . . . . . 14
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
145 | 144 | fveq2i 6759 |
. . . . . . . . . . . . 13
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
146 | | fvexd 6771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
147 | 98 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V) |
148 | 141, 142,
143, 18, 145, 66, 66, 67, 146, 147 | ressprdsds 23432 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))))) |
149 | 128 | ixpeq2dva 8658 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → X𝑥 ∈
𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
150 | 69 | cbvmptv 5183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)) |
151 | 150 | oveq2i 7266 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
152 | 24, 151 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
153 | 152 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
154 | 18, 153 | syl5eq 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
155 | 154 | fveq2d 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ball‘𝐷) =
(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))) |
156 | 155 | oveqdr 7283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟)) |
157 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
158 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
159 | 152 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
160 | 27, 159 | syl5eq 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
162 | 89, 161 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
163 | | rpgt0 12671 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
164 | 163 | ad2antll 725 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) |
165 | 151, 157,
10, 11, 158, 66, 67, 146, 86, 162, 123, 164 | prdsbl 23553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
166 | 156, 165 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
167 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
168 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
169 | 168 | ralrimiva 3107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
170 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
171 | 167, 143,
66, 67, 169, 170 | prdsbas3 17109 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
172 | 149, 166,
171 | 3eqtr4rd 2789 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
173 | 172 | sqxpeqd 5612 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
174 | 173 | reseq2d 5880 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
175 | 148, 174 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
176 | 144 | fveq2i 6759 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
177 | 176, 172 | syl5eq 2791 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
178 | 177 | fveq2d 6760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
179 | 140, 175,
178 | 3eltr3d 2853 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
180 | 47, 48, 60, 179 | syl12anc 833 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
181 | | totbndss 35862 |
. . . . . . . . 9
⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
182 | 180, 42, 181 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
183 | 46, 182 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴)) |
184 | 41, 183 | rexlimddv 3219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴)) |
185 | 184 | exp32 420 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
186 | 185 | exlimdv 1937 |
. . . 4
⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
187 | 6, 186 | syl5bi 241 |
. . 3
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
188 | 5, 187 | pm2.61dne 3030 |
. 2
⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
189 | 1, 188 | impbid2 225 |
1
⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) |