Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prdsbnd2 Structured version   Visualization version   GIF version

Theorem prdsbnd2 33907
Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.)
Hypotheses
Ref Expression
prdsbnd.y 𝑌 = (𝑆Xs𝑅)
prdsbnd.b 𝐵 = (Base‘𝑌)
prdsbnd.v 𝑉 = (Base‘(𝑅𝑥))
prdsbnd.e 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
prdsbnd.d 𝐷 = (dist‘𝑌)
prdsbnd.s (𝜑𝑆𝑊)
prdsbnd.i (𝜑𝐼 ∈ Fin)
prdsbnd.r (𝜑𝑅 Fn 𝐼)
prdsbnd2.c 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
prdsbnd2.e ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
prdsbnd2.m ((𝜑𝑥𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))
Assertion
Ref Expression
prdsbnd2 (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))
Distinct variable groups:   𝑦,𝐷   𝑥,𝑦,𝑅   𝑥,𝐵,𝑦   𝑦,𝐸   𝜑,𝑥,𝑦   𝑥,𝐼,𝑦   𝑥,𝑆   𝑦,𝑉   𝑥,𝑌
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥)   𝑆(𝑦)   𝐸(𝑥)   𝑉(𝑥)   𝑊(𝑥,𝑦)   𝑌(𝑦)

Proof of Theorem prdsbnd2
Dummy variables 𝑟 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 totbndbnd 33901 . 2 (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2 bndmet 33893 . . . . 5 (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3 0totbnd 33885 . . . . 5 (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
42, 3syl5ibr 236 . . . 4 (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
54a1i 11 . . 3 (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6 n0 4074 . . . 4 (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎𝐴)
7 simprr 813 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴))
8 eqid 2760 . . . . . . . . . . . 12 (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
9 eqid 2760 . . . . . . . . . . . 12 (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
10 prdsbnd.v . . . . . . . . . . . 12 𝑉 = (Base‘(𝑅𝑥))
11 prdsbnd.e . . . . . . . . . . . 12 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
12 eqid 2760 . . . . . . . . . . . 12 (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
13 prdsbnd.s . . . . . . . . . . . 12 (𝜑𝑆𝑊)
14 prdsbnd.i . . . . . . . . . . . 12 (𝜑𝐼 ∈ Fin)
15 fvexd 6364 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → (𝑅𝑥) ∈ V)
16 prdsbnd2.e . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
178, 9, 10, 11, 12, 13, 14, 15, 16prdsmet 22376 . . . . . . . . . . 11 (𝜑 → (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
18 prdsbnd.d . . . . . . . . . . . 12 𝐷 = (dist‘𝑌)
19 prdsbnd.y . . . . . . . . . . . . . 14 𝑌 = (𝑆Xs𝑅)
20 prdsbnd.r . . . . . . . . . . . . . . . 16 (𝜑𝑅 Fn 𝐼)
21 dffn5 6403 . . . . . . . . . . . . . . . 16 (𝑅 Fn 𝐼𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
2220, 21sylib 208 . . . . . . . . . . . . . . 15 (𝜑𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
2322oveq2d 6829 . . . . . . . . . . . . . 14 (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2419, 23syl5eq 2806 . . . . . . . . . . . . 13 (𝜑𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2524fveq2d 6356 . . . . . . . . . . . 12 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2618, 25syl5eq 2806 . . . . . . . . . . 11 (𝜑𝐷 = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
27 prdsbnd.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑌)
2824fveq2d 6356 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2927, 28syl5eq 2806 . . . . . . . . . . . 12 (𝜑𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
3029fveq2d 6356 . . . . . . . . . . 11 (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
3117, 26, 303eltr4d 2854 . . . . . . . . . 10 (𝜑𝐷 ∈ (Met‘𝐵))
3231adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33 simpr 479 . . . . . . . . . . 11 ((𝑎𝐴𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34 prdsbnd2.c . . . . . . . . . . . 12 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
3534bnd2lem 33903 . . . . . . . . . . 11 ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴𝐵)
3631, 33, 35syl2an 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝐴𝐵)
37 simprl 811 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝑎𝐴)
3836, 37sseldd 3745 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝑎𝐵)
3934ssbnd 33900 . . . . . . . . 9 ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
4032, 38, 39syl2anc 696 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
417, 40mpbid 222 . . . . . . 7 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42 simprr 813 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43 xpss12 5281 . . . . . . . . . . 11 ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
4442, 42, 43syl2anc 696 . . . . . . . . . 10 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
4544resabs1d 5586 . . . . . . . . 9 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
4645, 34syl6eqr 2812 . . . . . . . 8 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶)
47 simpll 807 . . . . . . . . . 10 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑)
4838adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎𝐵)
49 simprl 811 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ)
5037adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎𝐴)
5142, 50sseldd 3745 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52 ne0i 4064 . . . . . . . . . . . . 13 (𝑎 ∈ (𝑎(ball‘𝐷)𝑟) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
5351, 52syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
5431ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
55 metxmet 22340 . . . . . . . . . . . . . 14 (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
5654, 55syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
5749rexrd 10281 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ*)
58 xbln0 22420 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎𝐵𝑟 ∈ ℝ*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
5956, 48, 57, 58syl3anc 1477 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
6053, 59mpbid 222 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
6149, 60elrpd 12062 . . . . . . . . . 10 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ+)
62 eqid 2760 . . . . . . . . . . . 12 (𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))) = (𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))
63 eqid 2760 . . . . . . . . . . . 12 (Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))))
64 eqid 2760 . . . . . . . . . . . 12 (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥))
65 eqid 2760 . . . . . . . . . . . 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‘(𝑅𝑦)))))𝑟)))‘𝑥))))
66 eqid 2760 . . . . . . . . . . . 12 (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))))
6713adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑆𝑊)
6814adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
69 ovex 6841 . . . . . . . . . . . . . 14 ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)) ∈ V
70 fveq2 6352 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (𝑅𝑦) = (𝑅𝑥))
7170fveq2d 6356 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (dist‘(𝑅𝑦)) = (dist‘(𝑅𝑥)))
7270fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Base‘(𝑅𝑦)) = (Base‘(𝑅𝑥)))
7372, 10syl6eqr 2812 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (Base‘(𝑅𝑦)) = 𝑉)
7473sqxpeqd 5298 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦))) = (𝑉 × 𝑉))
7571, 74reseq12d 5552 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → ((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))) = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉)))
7675, 11syl6eqr 2812 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))) = 𝐸)
7776fveq2d 6356 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦))))) = (ball‘𝐸))
78 fveq2 6352 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (𝑎𝑦) = (𝑎𝑥))
79 eqidd 2761 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥𝑟 = 𝑟)
8077, 78, 79oveq123d 6834 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟) = ((𝑎𝑥)(ball‘𝐸)𝑟))
8170, 80oveq12d 6831 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)) = ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
8281cbvmptv 4902 . . . . . . . . . . . . . 14 (𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))) = (𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
8369, 82fnmpti 6183 . . . . . . . . . . . . 13 (𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))) Fn 𝐼
8483a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))) Fn 𝐼)
8516adantlr 753 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
86 metxmet 22340 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
8785, 86syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
8815ralrimiva 3104 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝐼 (𝑅𝑥) ∈ V)
8988adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → ∀𝑥𝐼 (𝑅𝑥) ∈ V)
90 simprl 811 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑎𝐵)
9129adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
9290, 91eleqtrd 2841 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
938, 9, 67, 68, 89, 10, 92prdsbascl 16345 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → ∀𝑥𝐼 (𝑎𝑥) ∈ 𝑉)
9493r19.21bi 3070 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝑎𝑥) ∈ 𝑉)
95 simplrr 820 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝑟 ∈ ℝ+)
9695rpred 12065 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝑟 ∈ ℝ)
97 blbnd 33899 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎𝑥) ∈ 𝑉𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
9887, 94, 96, 97syl3anc 1477 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
99 ovex 6841 . . . . . . . . . . . . . . . 16 ((𝑎𝑥)(ball‘𝐸)𝑟) ∈ V
100 xpeq12 5291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)))
101100anidms 680 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)))
102101reseq2d 5551 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))))
103 fveq2 6352 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
104102, 103eleq12d 2833 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟))))
105 fveq2 6352 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
106102, 105eleq12d 2833 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟))))
107104, 106bibi12d 334 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))))
108107imbi2d 329 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑎𝑥)(ball‘𝐸)𝑟) → (((𝜑𝑥𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑𝑥𝐼) → ((𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟))))))
109 prdsbnd2.m . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))
11099, 108, 109vtocl 3399 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → ((𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟))))
111110adantlr 753 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎𝑥)(ball‘𝐸)𝑟))))
11298, 111mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
113 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))) = (𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))
11481, 113, 69fvmpt 6444 . . . . . . . . . . . . . . . . . 18 (𝑥𝐼 → ((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥) = ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
115114adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥) = ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
116115fveq2d 6356 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (dist‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
117 eqid 2760 . . . . . . . . . . . . . . . . . 18 ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)) = ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))
118 eqid 2760 . . . . . . . . . . . . . . . . . 18 (dist‘(𝑅𝑥)) = (dist‘(𝑅𝑥))
119117, 118ressds 16275 . . . . . . . . . . . . . . . . 17 (((𝑎𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅𝑥)) = (dist‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
12099, 119ax-mp 5 . . . . . . . . . . . . . . . 16 (dist‘(𝑅𝑥)) = (dist‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
121116, 120syl6eqr 2812 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (dist‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅𝑥)))
122115fveq2d 6356 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
123 rpxr 12033 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
124123ad2antll 767 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ*)
125124adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝑟 ∈ ℝ*)
126 blssm 22424 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎𝑥) ∈ 𝑉𝑟 ∈ ℝ*) → ((𝑎𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
12787, 94, 125, 126syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝑎𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
128117, 10ressbas2 16133 . . . . . . . . . . . . . . . . . 18 (((𝑎𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
129127, 128syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝑎𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
130122, 129eqtr4d 2797 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) = ((𝑎𝑥)(ball‘𝐸)𝑟))
131130sqxpeqd 5298 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥))) = (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)))
132121, 131reseq12d 5552 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((dist‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)))) = ((dist‘(𝑅𝑥)) ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))))
13311reseq1i 5547 . . . . . . . . . . . . . . 15 (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)))
134 xpss12 5281 . . . . . . . . . . . . . . . . 17 ((((𝑎𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135127, 127, 134syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
136135resabs1d 5586 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅𝑥)) ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))))
137133, 136syl5eq 2806 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅𝑥)) ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))))
138132, 137eqtr4d 2797 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((dist‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎𝑥)(ball‘𝐸)𝑟) × ((𝑎𝑥)(ball‘𝐸)𝑟))))
139130fveq2d 6356 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (TotBnd‘(Base‘((𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎𝑥)(ball‘𝐸)𝑟)))
140112, 138, 1393eltr4d 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‘(𝑅𝑦)))))𝑟)))‘𝑥))))
14162, 63, 64, 65, 66, 67, 68, 84, 140prdstotbnd 33906 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))))))
14224adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
143 eqidd 2761 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))))
144 eqid 2760 . . . . . . . . . . . . 13 (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))))
14582oveq2i 6824 . . . . . . . . . . . . . 14 (𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))) = (𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
146145fveq2i 6355 . . . . . . . . . . . . 13 (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))))
147 fvexd 6364 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝑅𝑥) ∈ V)
14899a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝑎𝑥)(ball‘𝐸)𝑟) ∈ V)
149142, 143, 144, 18, 146, 67, 67, 68, 147, 148ressprdsds 22377 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))))))
150129ixpeq2dva 8089 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → X𝑥𝐼 ((𝑎𝑥)(ball‘𝐸)𝑟) = X𝑥𝐼 (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
15170cbvmptv 4902 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐼 ↦ (𝑅𝑦)) = (𝑥𝐼 ↦ (𝑅𝑥))
152151oveq2i 6824 . . . . . . . . . . . . . . . . . . . . 21 (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
15324, 152syl6eqr 2812 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑌 = (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
154153fveq2d 6356 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
15518, 154syl5eq 2806 . . . . . . . . . . . . . . . . . 18 (𝜑𝐷 = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
156155fveq2d 6356 . . . . . . . . . . . . . . . . 17 (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))))
157156oveqdr 6837 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟))
158 eqid 2760 . . . . . . . . . . . . . . . . 17 (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
159 eqid 2760 . . . . . . . . . . . . . . . . 17 (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
160153fveq2d 6356 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
16127, 160syl5eq 2806 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
162161adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
16390, 162eleqtrd 2841 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 𝑎 ∈ (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
164 rpgt0 12037 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ+ → 0 < 𝑟)
165164ad2antll 767 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → 0 < 𝑟)
166152, 158, 10, 11, 159, 67, 68, 147, 87, 163, 124, 165prdsbl 22497 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝑎(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟) = X𝑥𝐼 ((𝑎𝑥)(ball‘𝐸)𝑟))
167157, 166eqtrd 2794 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝑎(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑎𝑥)(ball‘𝐸)𝑟))
168 eqid 2760 . . . . . . . . . . . . . . . 16 (𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))) = (𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
16969a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)) ∈ V)
170169ralrimiva 3104 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → ∀𝑥𝐼 ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)) ∈ V)
171 eqid 2760 . . . . . . . . . . . . . . . 16 (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))
172168, 144, 67, 68, 170, 171prdsbas3 16343 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) = X𝑥𝐼 (Base‘((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))
173150, 167, 1723eqtr4rd 2805 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
174173sqxpeqd 5298 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → ((Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
175174reseq2d 5551 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝐷 ↾ ((Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176149, 175eqtrd 2794 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (dist‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
177145fveq2i 6355 . . . . . . . . . . . . 13 (Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ ((𝑅𝑥) ↾s ((𝑎𝑥)(ball‘𝐸)𝑟)))))
178177, 173syl5eq 2806 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
179178fveq2d 6356 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (TotBnd‘(Base‘(𝑆Xs(𝑦𝐼 ↦ ((𝑅𝑦) ↾s ((𝑎𝑦)(ball‘((dist‘(𝑅𝑦)) ↾ ((Base‘(𝑅𝑦)) × (Base‘(𝑅𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180141, 176, 1793eltr3d 2853 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑟 ∈ ℝ+)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
18147, 48, 61, 180syl12anc 1475 . . . . . . . . 9 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
182 totbndss 33889 . . . . . . . . 9 (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
183181, 42, 182syl2anc 696 . . . . . . . 8 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
18446, 183eqeltrrd 2840 . . . . . . 7 (((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
18541, 184rexlimddv 3173 . . . . . 6 ((𝜑 ∧ (𝑎𝐴𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
186185exp32 632 . . . . 5 (𝜑 → (𝑎𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187186exlimdv 2010 . . . 4 (𝜑 → (∃𝑎 𝑎𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
1886, 187syl5bi 232 . . 3 (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
1895, 188pm2.61dne 3018 . 2 (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
1901, 189impbid2 216 1 (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  wss 3715  c0 4058   class class class wbr 4804  cmpt 4881   × cxp 5264  cres 5268   Fn wfn 6044  cfv 6049  (class class class)co 6813  Xcixp 8074  Fincfn 8121  cr 10127  0cc0 10128  *cxr 10265   < clt 10266  +crp 12025  Basecbs 16059  s cress 16060  distcds 16152  Xscprds 16308  ∞Metcxmt 19933  Metcme 19934  ballcbl 19935  TotBndctotbnd 33878  Bndcbnd 33879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-ec 7913  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-icc 12375  df-fz 12520  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-hom 16168  df-cco 16169  df-prds 16310  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-totbnd 33880  df-bnd 33891
This theorem is referenced by:  cnpwstotbnd  33909
  Copyright terms: Public domain W3C validator