Step | Hyp | Ref
| Expression |
1 | | lmcau.1 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | 1 | methaus 23672 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) |
3 | | lmfun 22528 |
. . . 4
⊢ (𝐽 ∈ Haus → Fun
(⇝𝑡‘𝐽)) |
4 | | funfvbrb 6923 |
. . . 4
⊢ (Fun
(⇝𝑡‘𝐽) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓))) |
5 | 2, 3, 4 | 3syl 18 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓))) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
7 | 1, 6 | lmmbr 24418 |
. . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦)))) |
8 | 7 | biimpa 477 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦))) |
9 | 8 | simp1d 1141 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (𝑋 ↑pm
ℂ)) |
10 | | simprr 770 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
11 | | simplll 772 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝐷 ∈ (∞Met‘𝑋)) |
12 | 8 | simp2d 1142 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) →
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) |
13 | 12 | ad2antrr 723 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) |
14 | | rpre 12735 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
15 | 14 | ad2antlr 724 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑥 ∈ ℝ) |
16 | | uzid 12594 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
17 | 16 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑗 ∈ (ℤ≥‘𝑗)) |
18 | 17 | fvresd 6789 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) = (𝑓‘𝑗)) |
19 | 10, 17 | ffvelrnd 6957 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
20 | 18, 19 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
21 | | blhalf 23554 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧
((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) ∧ (𝑥 ∈ ℝ ∧ (𝑓‘𝑗) ∈
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
22 | 11, 13, 15, 20, 21 | syl22anc 836 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
23 | 10, 22 | fssd 6615 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
24 | | rphalfcl 12754 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
25 | 8 | simp3d 1143 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦)) |
26 | | oveq2 7277 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 / 2) →
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) =
(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
27 | 26 | feq3d 6584 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 / 2) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ (𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
28 | 27 | rexbidv 3228 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 / 2) → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
29 | 28 | rspcv 3556 |
. . . . . . . . . 10
⊢ ((𝑥 / 2) ∈ ℝ+
→ (∀𝑦 ∈
ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
30 | 24, 25, 29 | syl2im 40 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((𝐷 ∈
(∞Met‘𝑋) ∧
𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
31 | 30 | impcom 408 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
32 | | uzf 12582 |
. . . . . . . . 9
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
33 | | ffn 6597 |
. . . . . . . . 9
⊢
(ℤ≥:ℤ⟶𝒫 ℤ →
ℤ≥ Fn ℤ) |
34 | | reseq2 5884 |
. . . . . . . . . . 11
⊢ (𝑢 =
(ℤ≥‘𝑗) → (𝑓 ↾ 𝑢) = (𝑓 ↾ (ℤ≥‘𝑗))) |
35 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑢 =
(ℤ≥‘𝑗) → 𝑢 = (ℤ≥‘𝑗)) |
36 | 34, 35 | feq12d 6585 |
. . . . . . . . . 10
⊢ (𝑢 =
(ℤ≥‘𝑗) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
37 | 36 | rexrn 6958 |
. . . . . . . . 9
⊢
(ℤ≥ Fn ℤ → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) |
38 | 32, 33, 37 | mp2b 10 |
. . . . . . . 8
⊢
(∃𝑢 ∈ ran
ℤ≥(𝑓
↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
39 | 31, 38 | sylib 217 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℤ
(𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))) |
40 | 23, 39 | reximddv 3206 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℤ
(𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
41 | 40 | ralrimiva 3110 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)) |
42 | | iscau 24436 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)))) |
43 | 42 | adantr 481 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥)))) |
44 | 9, 41, 43 | mpbir2and 710 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (Cau‘𝐷)) |
45 | 44 | ex 413 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) → 𝑓 ∈ (Cau‘𝐷))) |
46 | 5, 45 | sylbid 239 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom
(⇝𝑡‘𝐽) → 𝑓 ∈ (Cau‘𝐷))) |
47 | 46 | ssrdv 3932 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → dom
(⇝𝑡‘𝐽) ⊆ (Cau‘𝐷)) |