Proof of Theorem dvres3a
Step | Hyp | Ref
| Expression |
1 | | reldv 23825 |
. . 3
⊢ Rel
(𝑆 D (𝐹 ↾ 𝑆)) |
2 | | recnprss 23859 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
3 | 2 | ad2antrr 764 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝑆 ⊆ ℂ) |
4 | | simplr 809 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐹:𝐴⟶ℂ) |
5 | | inss2 3969 |
. . . . . . 7
⊢ (𝑆 ∩ 𝐴) ⊆ 𝐴 |
6 | | fssres 6223 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑆 ∩ 𝐴) ⊆ 𝐴) → (𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ) |
7 | 4, 5, 6 | sylancl 697 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ) |
8 | | rescom 5573 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑆) = ((𝐹 ↾ 𝑆) ↾ 𝐴) |
9 | | resres 5559 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝑆) ↾ 𝐴) = (𝐹 ↾ (𝑆 ∩ 𝐴)) |
10 | 8, 9 | eqtri 2774 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑆) = (𝐹 ↾ (𝑆 ∩ 𝐴)) |
11 | | ffn 6198 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
12 | | fnresdm 6153 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
13 | 4, 11, 12 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ 𝐴) = 𝐹) |
14 | 13 | reseq1d 5542 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝐹 ↾ 𝐴) ↾ 𝑆) = (𝐹 ↾ 𝑆)) |
15 | 10, 14 | syl5eqr 2800 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ (𝑆 ∩ 𝐴)) = (𝐹 ↾ 𝑆)) |
16 | 15 | feq1d 6183 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝐹 ↾ (𝑆 ∩ 𝐴)):(𝑆 ∩ 𝐴)⟶ℂ ↔ (𝐹 ↾ 𝑆):(𝑆 ∩ 𝐴)⟶ℂ)) |
17 | 7, 16 | mpbid 222 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝐹 ↾ 𝑆):(𝑆 ∩ 𝐴)⟶ℂ) |
18 | | inss1 3968 |
. . . . . 6
⊢ (𝑆 ∩ 𝐴) ⊆ 𝑆 |
19 | 18 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 ∩ 𝐴) ⊆ 𝑆) |
20 | 3, 17, 19 | dvbss 23856 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ (𝑆 ∩ 𝐴)) |
21 | | dmres 5569 |
. . . . 5
⊢ dom
((ℂ D 𝐹) ↾
𝑆) = (𝑆 ∩ dom (ℂ D 𝐹)) |
22 | | simprr 813 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (ℂ D 𝐹) = 𝐴) |
23 | 22 | ineq2d 3949 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 ∩ dom (ℂ D 𝐹)) = (𝑆 ∩ 𝐴)) |
24 | 21, 23 | syl5eq 2798 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom ((ℂ D 𝐹) ↾ 𝑆) = (𝑆 ∩ 𝐴)) |
25 | 20, 24 | sseqtr4d 3775 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ dom ((ℂ D 𝐹) ↾ 𝑆)) |
26 | | relssres 5587 |
. . 3
⊢ ((Rel
(𝑆 D (𝐹 ↾ 𝑆)) ∧ dom (𝑆 D (𝐹 ↾ 𝑆)) ⊆ dom ((ℂ D 𝐹) ↾ 𝑆)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = (𝑆 D (𝐹 ↾ 𝑆))) |
27 | 1, 25, 26 | sylancr 698 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = (𝑆 D (𝐹 ↾ 𝑆))) |
28 | | dvfg 23861 |
. . . . 5
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ) |
29 | 28 | ad2antrr 764 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ) |
30 | | ffun 6201 |
. . . 4
⊢ ((𝑆 D (𝐹 ↾ 𝑆)):dom (𝑆 D (𝐹 ↾ 𝑆))⟶ℂ → Fun (𝑆 D (𝐹 ↾ 𝑆))) |
31 | 29, 30 | syl 17 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → Fun (𝑆 D (𝐹 ↾ 𝑆))) |
32 | | ssid 3757 |
. . . . 5
⊢ ℂ
⊆ ℂ |
33 | 32 | a1i 11 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ℂ ⊆
ℂ) |
34 | | dvres3a.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
35 | 34 | cnfldtopon 22779 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
36 | | simprl 811 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐴 ∈ 𝐽) |
37 | | toponss 20925 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ ℂ) |
38 | 35, 36, 37 | sylancr 698 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → 𝐴 ⊆ ℂ) |
39 | | dvres2 23867 |
. . . 4
⊢
(((ℂ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ ℂ)) → ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) |
40 | 33, 4, 38, 3, 39 | syl22anc 1474 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) |
41 | | funssres 6083 |
. . 3
⊢ ((Fun
(𝑆 D (𝐹 ↾ 𝑆)) ∧ ((ℂ D 𝐹) ↾ 𝑆) ⊆ (𝑆 D (𝐹 ↾ 𝑆))) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |
42 | 31, 40, 41 | syl2anc 696 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → ((𝑆 D (𝐹 ↾ 𝑆)) ↾ dom ((ℂ D 𝐹) ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |
43 | 27, 42 | eqtr3d 2788 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) |