Step | Hyp | Ref
| Expression |
1 | | totbndbnd 32758 |
. 2
⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴)) |
2 | | bndmet 32750 |
. . . . 5
⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴)) |
3 | | 0totbnd 32742 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴))) |
4 | 2, 3 | syl5ibr 235 |
. . . 4
⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
6 | | n0 3890 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔
∃𝑎 𝑎 ∈ 𝐴) |
7 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴)) |
8 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
9 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
10 | | prdsbnd.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Base‘(𝑅‘𝑥)) |
11 | | prdsbnd.e |
. . . . . . . . . . . 12
⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) |
12 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
13 | | prdsbnd.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
14 | | prdsbnd.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ Fin) |
15 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝑅‘𝑥) ∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
17 | | prdsbnd2.e |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
18 | 8, 9, 10, 11, 12, 13, 14, 16, 17 | prdsmet 21985 |
. . . . . . . . . . 11
⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
19 | | prdsbnd.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝑌) |
20 | | prdsbnd.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 = (𝑆Xs𝑅) |
21 | | prdsbnd.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 Fn 𝐼) |
22 | | dffn5 6151 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
25 | 20, 24 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
27 | 19, 26 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
28 | | prdsbnd.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑌) |
29 | 25 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
30 | 28, 29 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (Met‘𝐵) =
(Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
32 | 18, 27, 31 | 3eltr4d 2703 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵)) |
34 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴)) |
35 | | prdsbnd2.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) |
36 | 35 | bnd2lem 32760 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵) |
37 | 32, 34, 36 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵) |
38 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴) |
39 | 37, 38 | sseldd 3569 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵) |
40 | 35 | ssbnd 32757 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
41 | 33, 39, 40 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
42 | 7, 41 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
43 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
44 | | xpss12 5148 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
45 | 43, 43, 44 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
46 | 45 | resabs1d 5348 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴))) |
47 | 46, 35 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶) |
48 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑) |
49 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵) |
50 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ) |
51 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴) |
52 | 43, 51 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟)) |
53 | | ne0i 3880 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝑎(ball‘𝐷)𝑟) → (𝑎(ball‘𝐷)𝑟) ≠ ∅) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅) |
55 | 32 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵)) |
56 | | metxmet 21949 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵)) |
58 | 50 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ*) |
59 | | xbln0 22029 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
60 | 57, 49, 58, 59 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
61 | 54, 60 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟) |
62 | 50, 61 | elrpd 11745 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ+) |
63 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) |
64 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) |
65 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘((𝑦
∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) |
66 | | eqid 2610 |
. . . . . . . . . . . 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‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) |
67 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) |
68 | 13 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑆 ∈ 𝑊) |
69 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) |
70 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V |
71 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥))) |
73 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥))) |
74 | 73, 10 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉) |
75 | 74 | sqxpeqd 5065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉)) |
76 | 72, 75 | reseq12d 5318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))) |
77 | 76, 11 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸)) |
79 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥)) |
80 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟) |
81 | 78, 79, 80 | oveq123d 6570 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
82 | 71, 81 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
83 | 82 | cbvmptv 4678 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
84 | 70, 83 | fnmpti 5935 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼 |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼) |
86 | 17 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
87 | | metxmet 21949 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
89 | 16 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
91 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ 𝐵) |
92 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
93 | 91, 92 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
94 | 8, 9, 68, 69, 90, 10, 93 | prdsbascl 15966 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉) |
95 | 94 | r19.21bi 2916 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉) |
96 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ+) |
97 | 96 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ) |
98 | | blbnd 32756 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
99 | 88, 95, 97, 98 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
100 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V |
101 | | xpeq12 5058 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
102 | 101 | anidms 675 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
103 | 102 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
104 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
105 | 103, 104 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
106 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
107 | 103, 106 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
108 | 105, 107 | bibi12d 334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
109 | 108 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) |
110 | | prdsbnd2.m |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) |
111 | 100, 109,
110 | vtocl 3232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
112 | 111 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
113 | 99, 112 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
114 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) |
115 | 82, 114, 70 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
117 | 116 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
118 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
119 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥)) |
120 | 118, 119 | ressds 15896 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
121 | 100, 120 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
122 | 117, 121 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥))) |
123 | 116 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
124 | | rpxr 11716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
125 | 124 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
126 | 125 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ*) |
127 | | blssm 22033 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
128 | 88, 95, 126, 127 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
129 | 118, 10 | ressbas2 15758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
131 | 123, 130 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
132 | 131 | sqxpeqd 5065 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
133 | 122, 132 | reseq12d 5318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
134 | 11 | reseq1i 5313 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
135 | | xpss12 5148 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
136 | 128, 128,
135 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
137 | 136 | resabs1d 5348 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
138 | 134, 137 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
139 | 133, 138 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
140 | 131 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
141 | 113, 139,
140 | 3eltr4d 2703 |
. . . . . . . . . . . 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‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) |
142 | 63, 64, 65, 66, 67, 68, 69, 85, 141 | prdstotbnd 32763 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))))) |
143 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
144 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
145 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
146 | 83 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
147 | 146 | fveq2i 6106 |
. . . . . . . . . . . . 13
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
148 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
149 | 100 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V) |
150 | 143, 144,
145, 19, 147, 68, 68, 69, 148, 149 | ressprdsds 21986 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))))) |
151 | 130 | ixpeq2dva 7809 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → X𝑥 ∈
𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
152 | 71 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)) |
153 | 152 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
154 | 25, 153 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
155 | 154 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
156 | 19, 155 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
157 | 156 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ball‘𝐷) =
(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))) |
158 | 157 | oveqdr 6573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟)) |
159 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
160 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
161 | 154 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
162 | 28, 161 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
164 | 91, 163 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
165 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
166 | 165 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) |
167 | 153, 159,
10, 11, 160, 68, 69, 148, 88, 164, 125, 166 | prdsbl 22106 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
168 | 158, 167 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
169 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
170 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
171 | 170 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
172 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
173 | 169, 145,
68, 69, 171, 172 | prdsbas3 15964 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
174 | 151, 168,
173 | 3eqtr4rd 2655 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
175 | 174 | sqxpeqd 5065 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
176 | 175 | reseq2d 5317 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
177 | 150, 176 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
178 | 146 | fveq2i 6106 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
179 | 178, 174 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
180 | 179 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
181 | 142, 177,
180 | 3eltr3d 2702 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
182 | 48, 49, 62, 181 | syl12anc 1316 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
183 | | totbndss 32746 |
. . . . . . . . 9
⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
184 | 182, 43, 183 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
185 | 47, 184 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴)) |
186 | 42, 185 | rexlimddv 3017 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴)) |
187 | 186 | exp32 629 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
188 | 187 | exlimdv 1848 |
. . . 4
⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
189 | 6, 188 | syl5bi 231 |
. . 3
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
190 | 5, 189 | pm2.61dne 2868 |
. 2
⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
191 | 1, 190 | impbid2 215 |
1
⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) |