Step | Hyp | Ref
| Expression |
1 | | ulmss.u |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) |
2 | | ulmss.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 2 | uztrn2 12265 |
. . . . . . . 8
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
4 | | ulmss.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ 𝑆) |
5 | 4 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑇 ⊆ 𝑆) |
6 | | ssralv 4036 |
. . . . . . . . . 10
⊢ (𝑇 ⊆ 𝑆 → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
8 | | fvres 6692 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑇 → ((𝐴 ↾ 𝑇)‘𝑧) = (𝐴‘𝑧)) |
9 | 8 | ad2antll 727 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝐴 ↾ 𝑇)‘𝑧) = (𝐴‘𝑧)) |
10 | | simprl 769 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → 𝑥 ∈ 𝑍) |
11 | | ulmss.a |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) |
12 | 11 | adantrr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ 𝑊) |
13 | | resexg 5901 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑊 → (𝐴 ↾ 𝑇) ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (𝐴 ↾ 𝑇) ∈ V) |
15 | | eqid 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)) = (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)) |
16 | 15 | fvmpt2 6782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑍 ∧ (𝐴 ↾ 𝑇) ∈ V) → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = (𝐴 ↾ 𝑇)) |
17 | 10, 14, 16 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = (𝐴 ↾ 𝑇)) |
18 | 17 | fveq1d 6675 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = ((𝐴 ↾ 𝑇)‘𝑧)) |
19 | | eqid 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑍 ↦ 𝐴) = (𝑥 ∈ 𝑍 ↦ 𝐴) |
20 | 19 | fvmpt2 6782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑊) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
21 | 10, 12, 20 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
22 | 21 | fveq1d 6675 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) = (𝐴‘𝑧)) |
23 | 9, 18, 22 | 3eqtr4d 2869 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧)) |
24 | 23 | ralrimivva 3194 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧)) |
25 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) |
26 | | nfcv 2980 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑇 |
27 | | nffvmpt1 6684 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘) |
28 | | nfcv 2980 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝑧 |
29 | 27, 28 | nffv 6683 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) |
30 | | nffvmpt1 6684 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘) |
31 | 30, 28 | nffv 6683 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
32 | 29, 31 | nfeq 2994 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
33 | 26, 32 | nfralw 3228 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
34 | | fveq2 6673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)) |
35 | 34 | fveq1d 6675 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧)) |
36 | | fveq2 6673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)) |
37 | 36 | fveq1d 6675 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
38 | 35, 37 | eqeq12d 2840 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧))) |
39 | 38 | ralbidv 3200 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧))) |
40 | 25, 33, 39 | cbvralw 3444 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ ∀𝑘 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
41 | 24, 40 | sylib 220 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
42 | 41 | r19.21bi 3211 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
43 | | fvoveq1 7182 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧)))) |
44 | 43 | breq1d 5079 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
45 | 44 | ralimi 3163 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → ∀𝑧 ∈ 𝑇 ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
46 | | ralbi 3170 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑇 ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟) → (∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
47 | 42, 45, 46 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
48 | 7, 47 | sylibrd 261 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
49 | 3, 48 | sylan2 594 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
50 | 49 | anassrs 470 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
51 | 50 | ralimdva 3180 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
52 | 51 | reximdva 3277 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
53 | 52 | ralimdv 3181 |
. . 3
⊢ (𝜑 → (∀𝑟 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
54 | | ulmf 24973 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → ∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)) |
55 | 1, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)) |
56 | | fdm 6525 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ dom (𝑥 ∈ 𝑍 ↦ 𝐴) = (ℤ≥‘𝑚)) |
57 | 19 | dmmptss 6098 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ 𝑍 |
58 | 56, 57 | eqsstrrdi 4025 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ (ℤ≥‘𝑚) ⊆ 𝑍) |
59 | | uzid 12261 |
. . . . . . . 8
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
60 | 59 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ (ℤ≥‘𝑚)) |
61 | | ssel 3964 |
. . . . . . . 8
⊢
((ℤ≥‘𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ≥‘𝑚) → 𝑚 ∈ 𝑍)) |
62 | | eluzel2 12251 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
63 | 62, 2 | eleq2s 2934 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ ℤ) |
64 | 61, 63 | syl6 35 |
. . . . . . 7
⊢
((ℤ≥‘𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ≥‘𝑚) → 𝑀 ∈ ℤ)) |
65 | 58, 60, 64 | syl2imc 41 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ 𝑀 ∈
ℤ)) |
66 | 65 | rexlimdva 3287 |
. . . . 5
⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ 𝑀 ∈
ℤ)) |
67 | 55, 66 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
68 | 11 | ralrimiva 3185 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐴 ∈ 𝑊) |
69 | 19 | fnmpt 6491 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑍 𝐴 ∈ 𝑊 → (𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍) |
70 | 68, 69 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍) |
71 | | frn 6523 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ ↑m 𝑆)) |
72 | 71 | rexlimivw 3285 |
. . . . . 6
⊢
(∃𝑚 ∈
ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑m 𝑆)
→ ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ ↑m 𝑆)) |
73 | 55, 72 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ ↑m 𝑆)) |
74 | | df-f 6362 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶(ℂ ↑m 𝑆) ↔ ((𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍 ∧ ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ ↑m 𝑆))) |
75 | 70, 73, 74 | sylanbrc 585 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶(ℂ ↑m 𝑆)) |
76 | | eqidd 2825 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
77 | | eqidd 2825 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
78 | | ulmcl 24972 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
79 | 1, 78 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
80 | | ulmscl 24970 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) |
81 | 1, 80 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ V) |
82 | 2, 67, 75, 76, 77, 79, 81 | ulm2 24976 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
83 | 75 | fvmptelrn 6880 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ (ℂ ↑m 𝑆)) |
84 | | elmapi 8431 |
. . . . . . . 8
⊢ (𝐴 ∈ (ℂ
↑m 𝑆)
→ 𝐴:𝑆⟶ℂ) |
85 | 83, 84 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴:𝑆⟶ℂ) |
86 | 4 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑇 ⊆ 𝑆) |
87 | 85, 86 | fssresd 6548 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐴 ↾ 𝑇):𝑇⟶ℂ) |
88 | | cnex 10621 |
. . . . . . 7
⊢ ℂ
∈ V |
89 | 81, 4 | ssexd 5231 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
90 | 89 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑇 ∈ V) |
91 | | elmapg 8422 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑇 ∈ V)
→ ((𝐴 ↾ 𝑇) ∈ (ℂ
↑m 𝑇)
↔ (𝐴 ↾ 𝑇):𝑇⟶ℂ)) |
92 | 88, 90, 91 | sylancr 589 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝐴 ↾ 𝑇) ∈ (ℂ ↑m 𝑇) ↔ (𝐴 ↾ 𝑇):𝑇⟶ℂ)) |
93 | 87, 92 | mpbird 259 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐴 ↾ 𝑇) ∈ (ℂ ↑m 𝑇)) |
94 | 93 | fmpttd 6882 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)):𝑍⟶(ℂ ↑m 𝑇)) |
95 | | eqidd 2825 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧)) |
96 | | fvres 6692 |
. . . . 5
⊢ (𝑧 ∈ 𝑇 → ((𝐺 ↾ 𝑇)‘𝑧) = (𝐺‘𝑧)) |
97 | 96 | adantl 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → ((𝐺 ↾ 𝑇)‘𝑧) = (𝐺‘𝑧)) |
98 | 79, 4 | fssresd 6548 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ 𝑇):𝑇⟶ℂ) |
99 | 2, 67, 94, 95, 97, 98, 89 | ulm2 24976 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇) ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
100 | 53, 82, 99 | 3imtr4d 296 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇))) |
101 | 1, 100 | mpd 15 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) |