Step | Hyp | Ref
| Expression |
1 | | lmcau.1 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | 1 | methaus 22325 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) |
3 | | lmfun 21185 |
. . . 4
⊢ (𝐽 ∈ Haus → Fun
(⇝𝑡‘𝐽)) |
4 | | funfvbrb 6330 |
. . . 4
⊢ (Fun
(⇝𝑡‘𝐽) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓))) |
5 | 2, 3, 4 | 3syl 18 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓))) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
7 | 1, 6 | lmmbr 23056 |
. . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦)))) |
8 | 7 | biimpa 501 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦))) |
9 | 8 | simp1d 1073 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (𝑋 ↑pm
ℂ)) |
10 | | simprr 796 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
11 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝐷 ∈ (∞Met‘𝑋)) |
12 | 8 | simp2d 1074 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) →
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) |
13 | 12 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) |
14 | | rpre 11839 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
15 | 14 | ad2antlr 763 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑥 ∈ ℝ) |
16 | | uzid 11702 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
17 | 16 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑗 ∈ (ℤ≥‘𝑗)) |
18 | | fvres 6207 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) = (𝑓‘𝑗)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) = (𝑓‘𝑗)) |
20 | 10, 17 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
21 | 19, 20 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
22 | | blhalf 22210 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) ∧ (𝑥 ∈ ℝ ∧ (𝑓‘𝑗) ∈
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
23 | 11, 13, 15, 21, 22 | syl22anc 1327 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
24 | 10, 23 | fssd 6057 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
25 | | rphalfcl 11858 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
26 | 8 | simp3d 1075 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦)) |
27 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 / 2) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) =
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
28 | 27 | feq3d 6032 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 / 2) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ (𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
29 | 28 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 / 2) → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
30 | 29 | rspcv 3305 |
. . . . . . . . . 10
⊢ ((𝑥 / 2) ∈ ℝ+
→ (∀𝑦 ∈
ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
31 | 25, 26, 30 | syl2im 40 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((𝐷 ∈
(∞Met‘𝑋) ∧
𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
32 | 31 | impcom 446 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
33 | | uzf 11690 |
. . . . . . . . 9
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
34 | | ffn 6045 |
. . . . . . . . 9
⊢
(ℤ≥:ℤ⟶𝒫 ℤ →
ℤ≥ Fn ℤ) |
35 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑢 =
(ℤ≥‘𝑗) → (𝑓 ↾ 𝑢) = (𝑓 ↾ (ℤ≥‘𝑗))) |
36 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑢 =
(ℤ≥‘𝑗) → 𝑢 = (ℤ≥‘𝑗)) |
37 | 35, 36 | feq12d 6033 |
. . . . . . . . . 10
⊢ (𝑢 =
(ℤ≥‘𝑗) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
38 | 37 | rexrn 6361 |
. . . . . . . . 9
⊢
(ℤ≥ Fn ℤ → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
39 | 33, 34, 38 | mp2b 10 |
. . . . . . . 8
⊢
(∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
40 | 32, 39 | sylib 208 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℤ
(𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
41 | 24, 40 | reximddv 3018 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℤ
(𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
42 | 41 | ralrimiva 2966 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
43 | | iscau 23074 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)))) |
44 | 43 | adantr 481 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)))) |
45 | 9, 42, 44 | mpbir2and 957 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (Cau‘𝐷)) |
46 | 45 | ex 450 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) → 𝑓 ∈ (Cau‘𝐷))) |
47 | 5, 46 | sylbid 230 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) → 𝑓 ∈ (Cau‘𝐷))) |
48 | 47 | ssrdv 3609 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → dom
(⇝𝑡‘𝐽) ⊆ (Cau‘𝐷)) |