Proof of Theorem cpnres
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
2 | | simpr 476 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝐹 ∈
((Cn‘ℂ)‘𝑁)) |
3 | | ssid 3587 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
4 | | elfvdm 6130 |
. . . . . . . 8
⊢ (𝐹 ∈
((Cn‘ℂ)‘𝑁) → 𝑁 ∈ dom
(Cn‘ℂ)) |
5 | 4 | adantl 481 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑁 ∈ dom
(Cn‘ℂ)) |
6 | | fncpn 23502 |
. . . . . . . . 9
⊢ (ℂ
⊆ ℂ → (Cn‘ℂ) Fn
ℕ0) |
7 | 3, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(Cn‘ℂ) Fn
ℕ0 |
8 | | fndm 5904 |
. . . . . . . 8
⊢
((Cn‘ℂ) Fn ℕ0 → dom
(Cn‘ℂ) = ℕ0) |
9 | 7, 8 | mp1i 13 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → dom
(Cn‘ℂ) = ℕ0) |
10 | 5, 9 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑁 ∈
ℕ0) |
11 | | elcpn 23503 |
. . . . . 6
⊢ ((ℂ
⊆ ℂ ∧ 𝑁
∈ ℕ0) → (𝐹 ∈
((Cn‘ℂ)‘𝑁) ↔ (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)))) |
12 | 3, 10, 11 | sylancr 694 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ∈
((Cn‘ℂ)‘𝑁) ↔ (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)))) |
13 | 2, 12 | mpbid 221 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ))) |
14 | 13 | simpld 474 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
15 | | pmresg 7771 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
16 | 1, 14, 15 | syl2anc 691 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
17 | 13 | simprd 478 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((ℂ D𝑛
𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)) |
18 | | cncff 22504 |
. . . . . 6
⊢
(((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ) → ((ℂ D𝑛
𝐹)‘𝑁):dom 𝐹⟶ℂ) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((ℂ D𝑛
𝐹)‘𝑁):dom 𝐹⟶ℂ) |
20 | | fdm 5964 |
. . . . 5
⊢
(((ℂ D𝑛 𝐹)‘𝑁):dom 𝐹⟶ℂ → dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹) |
22 | | dvnres 23500 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
23 | 1, 14, 10, 21, 22 | syl31anc 1321 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
24 | | resres 5329 |
. . . . . . 7
⊢
((((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆) ↾ dom 𝐹) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) |
25 | | rescom 5343 |
. . . . . . 7
⊢
((((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆) ↾ dom 𝐹) = ((((ℂ D𝑛 𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) |
26 | 24, 25 | eqtr3i 2634 |
. . . . . 6
⊢
(((ℂ D𝑛 𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) = ((((ℂ D𝑛 𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) |
27 | | ffn 5958 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝐹)‘𝑁):dom 𝐹⟶ℂ → ((ℂ
D𝑛 𝐹)‘𝑁) Fn dom 𝐹) |
28 | | fnresdm 5914 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝐹)‘𝑁) Fn dom 𝐹 → (((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) = ((ℂ D𝑛 𝐹)‘𝑁)) |
29 | 19, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) = ((ℂ D𝑛 𝐹)‘𝑁)) |
30 | 29 | reseq1d 5316 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
31 | 26, 30 | syl5eq 2656 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
32 | | inss2 3796 |
. . . . . 6
⊢ (𝑆 ∩ dom 𝐹) ⊆ dom 𝐹 |
33 | | rescncf 22508 |
. . . . . 6
⊢ ((𝑆 ∩ dom 𝐹) ⊆ dom 𝐹 → (((ℂ D𝑛
𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ))) |
34 | 32, 17, 33 | mpsyl 66 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ)) |
35 | 31, 34 | eqeltrrd 2689 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ 𝑆) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ)) |
36 | | dmres 5339 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹) |
37 | 36 | oveq1i 6559 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝑆)–cn→ℂ) = ((𝑆 ∩ dom 𝐹)–cn→ℂ) |
38 | 35, 37 | syl6eleqr 2699 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ 𝑆) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)) |
39 | 23, 38 | eqeltrd 2688 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)) |
40 | | recnprss 23474 |
. . . 4
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
41 | 40 | adantr 480 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑆 ⊆ ℂ) |
42 | | elcpn 23503 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐹 ↾ 𝑆) ∈
((Cn‘𝑆)‘𝑁) ↔ ((𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)))) |
43 | 41, 10, 42 | syl2anc 691 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝐹 ↾ 𝑆) ∈ ((Cn‘𝑆)‘𝑁) ↔ ((𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)))) |
44 | 16, 39, 43 | mpbir2and 959 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ ((Cn‘𝑆)‘𝑁)) |