Proof of Theorem cpnres
Step | Hyp | Ref
| Expression |
1 | | simpl 474 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
2 | | simpr 479 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝐹 ∈
((Cn‘ℂ)‘𝑁)) |
3 | | ssid 3757 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
4 | | elfvdm 6373 |
. . . . . . . 8
⊢ (𝐹 ∈
((Cn‘ℂ)‘𝑁) → 𝑁 ∈ dom
(Cn‘ℂ)) |
5 | 4 | adantl 473 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑁 ∈ dom
(Cn‘ℂ)) |
6 | | fncpn 23887 |
. . . . . . . . 9
⊢ (ℂ
⊆ ℂ → (Cn‘ℂ) Fn
ℕ0) |
7 | 3, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(Cn‘ℂ) Fn
ℕ0 |
8 | | fndm 6143 |
. . . . . . . 8
⊢
((Cn‘ℂ) Fn ℕ0 → dom
(Cn‘ℂ) = ℕ0) |
9 | 7, 8 | mp1i 13 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → dom
(Cn‘ℂ) = ℕ0) |
10 | 5, 9 | eleqtrd 2833 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑁 ∈
ℕ0) |
11 | | elcpn 23888 |
. . . . . 6
⊢ ((ℂ
⊆ ℂ ∧ 𝑁
∈ ℕ0) → (𝐹 ∈
((Cn‘ℂ)‘𝑁) ↔ (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)))) |
12 | 3, 10, 11 | sylancr 698 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ∈
((Cn‘ℂ)‘𝑁) ↔ (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)))) |
13 | 2, 12 | mpbid 222 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ∈ (ℂ ↑pm
ℂ) ∧ ((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ))) |
14 | 13 | simpld 477 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
15 | | pmresg 8043 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
16 | 1, 14, 15 | syl2anc 696 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
17 | 13 | simprd 482 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((ℂ D𝑛
𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)) |
18 | | cncff 22889 |
. . . . . 6
⊢
(((ℂ D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ) → ((ℂ D𝑛
𝐹)‘𝑁):dom 𝐹⟶ℂ) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((ℂ D𝑛
𝐹)‘𝑁):dom 𝐹⟶ℂ) |
20 | | fdm 6204 |
. . . . 5
⊢
(((ℂ D𝑛 𝐹)‘𝑁):dom 𝐹⟶ℂ → dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹) |
22 | | dvnres 23885 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
23 | 1, 14, 10, 21, 22 | syl31anc 1476 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
24 | | resres 5559 |
. . . . . . 7
⊢
((((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆) ↾ dom 𝐹) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) |
25 | | rescom 5573 |
. . . . . . 7
⊢
((((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆) ↾ dom 𝐹) = ((((ℂ D𝑛 𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) |
26 | 24, 25 | eqtr3i 2776 |
. . . . . 6
⊢
(((ℂ D𝑛 𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) = ((((ℂ D𝑛 𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) |
27 | | ffn 6198 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝐹)‘𝑁):dom 𝐹⟶ℂ → ((ℂ
D𝑛 𝐹)‘𝑁) Fn dom 𝐹) |
28 | | fnresdm 6153 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝐹)‘𝑁) Fn dom 𝐹 → (((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) = ((ℂ D𝑛 𝐹)‘𝑁)) |
29 | 19, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) = ((ℂ D𝑛 𝐹)‘𝑁)) |
30 | 29 | reseq1d 5542 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((((ℂ D𝑛
𝐹)‘𝑁) ↾ dom 𝐹) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
31 | 26, 30 | syl5eq 2798 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
32 | | inss2 3969 |
. . . . . 6
⊢ (𝑆 ∩ dom 𝐹) ⊆ dom 𝐹 |
33 | | rescncf 22893 |
. . . . . 6
⊢ ((𝑆 ∩ dom 𝐹) ⊆ dom 𝐹 → (((ℂ D𝑛
𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ))) |
34 | 32, 17, 33 | mpsyl 68 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ (𝑆 ∩ dom 𝐹)) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ)) |
35 | 31, 34 | eqeltrrd 2832 |
. . . 4
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ 𝑆) ∈ ((𝑆 ∩ dom 𝐹)–cn→ℂ)) |
36 | | dmres 5569 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹) |
37 | 36 | oveq1i 6815 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝑆)–cn→ℂ) = ((𝑆 ∩ dom 𝐹)–cn→ℂ) |
38 | 35, 37 | syl6eleqr 2842 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (((ℂ D𝑛
𝐹)‘𝑁) ↾ 𝑆) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)) |
39 | 23, 38 | eqeltrd 2831 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)) |
40 | | recnprss 23859 |
. . . 4
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
41 | 40 | adantr 472 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → 𝑆 ⊆ ℂ) |
42 | | elcpn 23888 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐹 ↾ 𝑆) ∈
((Cn‘𝑆)‘𝑁) ↔ ((𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)))) |
43 | 41, 10, 42 | syl2anc 696 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → ((𝐹 ↾ 𝑆) ∈ ((Cn‘𝑆)‘𝑁) ↔ ((𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) ∈ (dom (𝐹 ↾ 𝑆)–cn→ℂ)))) |
44 | 16, 39, 43 | mpbir2and 995 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈
((Cn‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ ((Cn‘𝑆)‘𝑁)) |