Proof of Theorem dvres3a
Step | Hyp | Ref
| Expression |
1 | | reldv 23440 |
. . 3
⊢ Rel
(𝑆 D (𝐹 ↾ 𝑆)) |
2 | | recnprss 23474 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
3 | 2 | ad2antrr 758 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝑆 ⊆ ℂ) |
4 | | simplr 788 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐹:𝐴⟶ℂ) |
5 | | inss2 3796 |
. . . . . . 7
⊢ (𝑆 ∩ 𝐴) ⊆ 𝐴 |
6 | | fssres 5983 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑆 ∩ 𝐴) ⊆ 𝐴) → (𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ) |
7 | 4, 5, 6 | sylancl 693 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ) |
8 | | rescom 5343 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑆) = ((𝐹 ↾ 𝑆) ↾ 𝐴) |
9 | | resres 5329 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝑆) ↾ 𝐴) = (𝐹 ↾ (𝑆 ∩ 𝐴)) |
10 | 8, 9 | eqtri 2632 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑆) = (𝐹 ↾ (𝑆 ∩ 𝐴)) |
11 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
12 | | fnresdm 5914 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
13 | 4, 11, 12 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ 𝐴) = 𝐹) |
14 | 13 | reseq1d 5316 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝐹 ↾ 𝐴) ↾ 𝑆) = (𝐹 ↾ 𝑆)) |
15 | 10, 14 | syl5eqr 2658 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ (𝑆 ∩ 𝐴)) = (𝐹 ↾ 𝑆)) |
16 | 15 | feq1d 5943 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ ↔ (𝐹 ↾ 𝑆):(𝑆 ∩ 𝐴)⟶ℂ)) |
17 | 7, 16 | mpbid 221 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ 𝑆):(𝑆 ∩ 𝐴)⟶ℂ) |
18 | | inss1 3795 |
. . . . . 6
⊢ (𝑆 ∩ 𝐴) ⊆ 𝑆 |
19 | 18 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 ∩ 𝐴) ⊆ 𝑆) |
20 | 3, 17, 19 | dvbss 23471 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ (𝑆 ∩ 𝐴)) |
21 | | dmres 5339 |
. . . . 5
⊢ dom
((ℂ D 𝐹) ↾
𝑆) = (𝑆 ∩ dom (ℂ D 𝐹)) |
22 | | simprr 792 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (ℂ D 𝐹) = 𝐴) |
23 | 22 | ineq2d 3776 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 ∩ dom (ℂ D 𝐹)) = (𝑆 ∩ 𝐴)) |
24 | 21, 23 | syl5eq 2656 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom ((ℂ D 𝐹) ↾ 𝑆) = (𝑆 ∩ 𝐴)) |
25 | 20, 24 | sseqtr4d 3605 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ dom ((ℂ D 𝐹) ↾ 𝑆)) |
26 | | relssres 5357 |
. . 3
⊢ ((Rel
(𝑆 D (𝐹 ↾ 𝑆)) ∧ dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ dom ((ℂ D 𝐹) ↾ 𝑆)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = (𝑆 D (𝐹 ↾ 𝑆))) |
27 | 1, 25, 26 | sylancr 694 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = (𝑆 D (𝐹 ↾ 𝑆))) |
28 | | dvfg 23476 |
. . . . 5
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ) |
29 | 28 | ad2antrr 758 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ) |
30 | | ffun 5961 |
. . . 4
⊢ ((𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ → Fun (𝑆 D (𝐹 ↾ 𝑆))) |
31 | 29, 30 | syl 17 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → Fun (𝑆 D (𝐹 ↾ 𝑆))) |
32 | | ssid 3587 |
. . . . 5
⊢ ℂ
⊆ ℂ |
33 | 32 | a1i 11 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ℂ ⊆
ℂ) |
34 | | dvres3a.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
35 | 34 | cnfldtopon 22396 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
36 | | simprl 790 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐴 ∈ 𝐽) |
37 | | toponss 20544 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ℂ) |
38 | 35, 36, 37 | sylancr 694 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐴 ⊆ ℂ) |
39 | | dvres2 23482 |
. . . 4
⊢
(((ℂ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ ℂ)) → ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) |
40 | 33, 4, 38, 3, 39 | syl22anc 1319 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) |
41 | | funssres 5844 |
. . 3
⊢ ((Fun
(𝑆 D (𝐹 ↾ 𝑆)) ∧ ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |
42 | 31, 40, 41 | syl2anc 691 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |
43 | 27, 42 | eqtr3d 2646 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |