| Step | Hyp | Ref
| Expression |
| 1 | | totbndbnd 37796 |
. 2
⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴)) |
| 2 | | bndmet 37788 |
. . . . 5
⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴)) |
| 3 | | 0totbnd 37780 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴))) |
| 4 | 2, 3 | imbitrrid 246 |
. . . 4
⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
| 6 | | n0 4353 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔
∃𝑎 𝑎 ∈ 𝐴) |
| 7 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴)) |
| 8 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
| 9 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
| 10 | | prdsbnd.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Base‘(𝑅‘𝑥)) |
| 11 | | prdsbnd.e |
. . . . . . . . . . . 12
⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) |
| 12 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
| 13 | | prdsbnd.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
| 14 | | prdsbnd.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ Fin) |
| 15 | | fvexd 6921 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
| 16 | | prdsbnd2.e |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
| 17 | 8, 9, 10, 11, 12, 13, 14, 15, 16 | prdsmet 24380 |
. . . . . . . . . . 11
⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
| 18 | | prdsbnd.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝑌) |
| 19 | | prdsbnd.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 = (𝑆Xs𝑅) |
| 20 | | prdsbnd.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 Fn 𝐼) |
| 21 | | dffn5 6967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
| 23 | 22 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
| 24 | 19, 23 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
| 25 | 24 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 26 | 18, 25 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 27 | | prdsbnd.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑌) |
| 28 | 24 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 29 | 27, 28 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 → (Met‘𝐵) =
(Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
| 31 | 17, 26, 30 | 3eltr4d 2856 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵)) |
| 33 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴)) |
| 34 | | prdsbnd2.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) |
| 35 | 34 | bnd2lem 37798 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵) |
| 36 | 31, 33, 35 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵) |
| 37 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴) |
| 38 | 36, 37 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵) |
| 39 | 34 | ssbnd 37795 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
| 40 | 32, 38, 39 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) |
| 41 | 7, 40 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
| 42 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) |
| 43 | | xpss12 5700 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
| 44 | 42, 42, 43 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
| 45 | 44 | resabs1d 6026 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴))) |
| 46 | 45, 34 | eqtr4di 2795 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶) |
| 47 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑) |
| 48 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵) |
| 49 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ) |
| 50 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴) |
| 51 | 42, 50 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟)) |
| 52 | 51 | ne0d 4342 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅) |
| 53 | 31 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵)) |
| 54 | | metxmet 24344 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵)) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵)) |
| 56 | 49 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ*) |
| 57 | | xbln0 24424 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
| 58 | 55, 48, 56, 57 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
| 59 | 52, 58 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟) |
| 60 | 49, 59 | elrpd 13074 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ+) |
| 61 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) |
| 62 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) |
| 63 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘((𝑦
∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) |
| 64 | | eqid 2737 |
. . . . . . . . . . . 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 2737 |
. . . . . . . . . . . 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 7464 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V |
| 69 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
| 70 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥))) |
| 71 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥))) |
| 72 | 71, 10 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉) |
| 73 | 72 | sqxpeqd 5717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉)) |
| 74 | 70, 73 | reseq12d 5998 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))) |
| 75 | 74, 11 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸)) |
| 77 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥)) |
| 78 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟) |
| 79 | 76, 77, 78 | oveq123d 7452 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
| 80 | 69, 79 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 81 | 80 | cbvmptv 5255 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 82 | 68, 81 | fnmpti 6711 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼 |
| 83 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼) |
| 84 | 16 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
| 85 | | metxmet 24344 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
| 87 | 15 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
| 89 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ 𝐵) |
| 90 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 91 | 89, 90 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
| 92 | 8, 9, 66, 67, 88, 10, 91 | prdsbascl 17528 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉) |
| 93 | 92 | r19.21bi 3251 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉) |
| 94 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ+) |
| 95 | 94 | rpred 13077 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ) |
| 96 | | blbnd 37794 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 97 | 86, 93, 95, 96 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 98 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V |
| 99 | | xpeq12 5710 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 100 | 99 | anidms 566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 101 | 100 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 102 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 103 | 101, 102 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 104 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 105 | 101, 104 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . 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 3558 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 110 | 109 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 111 | 97, 110 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 112 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) |
| 113 | 80, 112, 68 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 114 | 113 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 115 | 114 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
| 117 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥)) |
| 118 | 116, 117 | ressds 17454 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 119 | 98, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 120 | 115, 119 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥))) |
| 121 | 114 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 122 | | rpxr 13044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 123 | 122 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
| 124 | 123 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ*) |
| 125 | | blssm 24428 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
| 126 | 86, 93, 124, 125 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) |
| 127 | 116, 10 | ressbas2 17283 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 129 | 121, 128 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
| 130 | 129 | sqxpeqd 5717 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 131 | 120, 130 | reseq12d 5998 |
. . . . . . . . . . . . . 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 5993 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 133 | | xpss12 5700 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
| 134 | 126, 126,
133 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉)) |
| 135 | 134 | resabs1d 6026 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 136 | 132, 135 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 137 | 131, 136 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 138 | 129 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 139 | 111, 137,
138 | 3eltr4d 2856 |
. . . . . . . . . . . 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 37801 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))))) |
| 141 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
| 142 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
| 143 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
| 144 | 81 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 145 | 144 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
| 146 | | fvexd 6921 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
| 147 | 98 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V) |
| 148 | 141, 142,
143, 18, 145, 66, 66, 67, 146, 147 | ressprdsds 24381 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))))) |
| 149 | 128 | ixpeq2dva 8952 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → X𝑥 ∈
𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 150 | 69 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)) |
| 151 | 150 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
| 152 | 24, 151 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
| 153 | 152 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 154 | 18, 153 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 155 | 154 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ball‘𝐷) =
(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))) |
| 156 | 155 | oveqdr 7459 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟)) |
| 157 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
| 158 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
| 159 | 152 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 160 | 27, 159 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 162 | 89, 161 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
| 163 | | rpgt0 13047 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
| 164 | 163 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) |
| 165 | 151, 157,
10, 11, 158, 66, 67, 146, 86, 162, 123, 164 | prdsbl 24504 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
| 166 | 156, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟)) |
| 167 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 168 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
| 169 | 168 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V) |
| 170 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) |
| 171 | 167, 143,
66, 67, 169, 170 | prdsbas3 17526 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) |
| 172 | 149, 166,
171 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
| 173 | 172 | sqxpeqd 5717 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) |
| 174 | 173 | reseq2d 5997 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
| 175 | 148, 174 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))) |
| 176 | 144 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) |
| 177 | 176, 172 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟)) |
| 178 | 177 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) →
(TotBnd‘(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
| 179 | 140, 175,
178 | 3eltr3d 2855 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
| 180 | 47, 48, 60, 179 | syl12anc 837 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟))) |
| 181 | | totbndss 37784 |
. . . . . . . . 9
⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
| 182 | 180, 42, 181 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴)) |
| 183 | 46, 182 | eqeltrrd 2842 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴)) |
| 184 | 41, 183 | rexlimddv 3161 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴)) |
| 185 | 184 | exp32 420 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
| 186 | 185 | exlimdv 1933 |
. . . 4
⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
| 187 | 6, 186 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))) |
| 188 | 5, 187 | pm2.61dne 3028 |
. 2
⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))) |
| 189 | 1, 188 | impbid2 226 |
1
⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) |