Step | Hyp | Ref
| Expression |
1 | | ulmscl 25548 |
. . . 4
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) |
2 | | ulmcl 25550 |
. . . 4
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
3 | 1, 2 | jca 512 |
. . 3
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ))) |
5 | | ulmscl 25548 |
. . . 4
⊢ ((𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) |
6 | | ulmcl 25550 |
. . . 4
⊢ ((𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
7 | 5, 6 | jca 512 |
. . 3
⊢ ((𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺 → (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) |
8 | 7 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺 → (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ))) |
9 | | ulmres.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
10 | | ulmres.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
11 | 9, 10 | eleqtrdi 2849 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
13 | | eluzel2 12597 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝑀 ∈ ℤ) |
15 | 10 | rexuz3 15070 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
17 | | eluzelz 12602 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
18 | 12, 17 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝑁 ∈ ℤ) |
19 | | ulmres.w |
. . . . . . . 8
⊢ 𝑊 =
(ℤ≥‘𝑁) |
20 | 19 | rexuz3 15070 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
21 | 18, 20 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
22 | 16, 21 | bitr4d 281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
23 | 22 | ralbidv 3121 |
. . . 4
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (∀𝑟 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
24 | | ulmres.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
25 | 24 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
26 | | eqidd 2739 |
. . . . 5
⊢ (((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑧)) |
27 | | eqidd 2739 |
. . . . 5
⊢ (((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
28 | | simprr 770 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝐺:𝑆⟶ℂ) |
29 | | simprl 768 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝑆 ∈ V) |
30 | 10, 14, 25, 26, 27, 28, 29 | ulm2 25554 |
. . . 4
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
31 | | uzss 12615 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
32 | 12, 31 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
33 | 32, 19, 10 | 3sstr4g 3965 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → 𝑊 ⊆ 𝑍) |
34 | 25, 33 | fssresd 6633 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (𝐹 ↾ 𝑊):𝑊⟶(ℂ ↑m 𝑆)) |
35 | | fvres 6785 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘𝑘) = (𝐹‘𝑘)) |
36 | 35 | ad2antrl 725 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → ((𝐹 ↾ 𝑊)‘𝑘) = (𝐹‘𝑘)) |
37 | 36 | fveq1d 6768 |
. . . . 5
⊢ (((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → (((𝐹 ↾ 𝑊)‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑧)) |
38 | 19, 18, 34, 37, 27, 28, 29 | ulm2 25554 |
. . . 4
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → ((𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
39 | 23, 30, 38 | 3bitr4d 311 |
. . 3
⊢ ((𝜑 ∧ (𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ)) → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ (𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺)) |
40 | 39 | ex 413 |
. 2
⊢ (𝜑 → ((𝑆 ∈ V ∧ 𝐺:𝑆⟶ℂ) → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ (𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺))) |
41 | 4, 8, 40 | pm5.21ndd 381 |
1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ (𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺)) |