Step |
Hyp |
Ref |
Expression |
1 |
|
dvres3a.j |
⊢ 𝐽 = ( TopOpen ‘ ℂfld ) |
2 |
|
reldv |
⊢ Rel ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) |
3 |
|
recnprss |
⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ ) |
4 |
3
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → 𝑆 ⊆ ℂ ) |
5 |
|
simplr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℂ ) |
6 |
|
inss2 |
⊢ ( 𝑆 ∩ 𝐴 ) ⊆ 𝐴 |
7 |
|
fssres |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝑆 ∩ 𝐴 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) : ( 𝑆 ∩ 𝐴 ) ⟶ ℂ ) |
8 |
5 6 7
|
sylancl |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) : ( 𝑆 ∩ 𝐴 ) ⟶ ℂ ) |
9 |
|
rescom |
⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑆 ) = ( ( 𝐹 ↾ 𝑆 ) ↾ 𝐴 ) |
10 |
|
resres |
⊢ ( ( 𝐹 ↾ 𝑆 ) ↾ 𝐴 ) = ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) |
11 |
9 10
|
eqtri |
⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑆 ) = ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) |
12 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 ) |
13 |
|
fnresdm |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
14 |
5 12 13
|
3syl |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
15 |
14
|
reseq1d |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑆 ) = ( 𝐹 ↾ 𝑆 ) ) |
16 |
11 15
|
syl5eqr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝑆 ) ) |
17 |
16
|
feq1d |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( ( 𝐹 ↾ ( 𝑆 ∩ 𝐴 ) ) : ( 𝑆 ∩ 𝐴 ) ⟶ ℂ ↔ ( 𝐹 ↾ 𝑆 ) : ( 𝑆 ∩ 𝐴 ) ⟶ ℂ ) ) |
18 |
8 17
|
mpbid |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝐹 ↾ 𝑆 ) : ( 𝑆 ∩ 𝐴 ) ⟶ ℂ ) |
19 |
|
inss1 |
⊢ ( 𝑆 ∩ 𝐴 ) ⊆ 𝑆 |
20 |
19
|
a1i |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝑆 ∩ 𝐴 ) ⊆ 𝑆 ) |
21 |
4 18 20
|
dvbss |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ ( 𝑆 ∩ 𝐴 ) ) |
22 |
|
dmres |
⊢ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) = ( 𝑆 ∩ dom ( ℂ D 𝐹 ) ) |
23 |
|
simprr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → dom ( ℂ D 𝐹 ) = 𝐴 ) |
24 |
23
|
ineq2d |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝑆 ∩ dom ( ℂ D 𝐹 ) ) = ( 𝑆 ∩ 𝐴 ) ) |
25 |
22 24
|
syl5eq |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) = ( 𝑆 ∩ 𝐴 ) ) |
26 |
21 25
|
sseqtrrd |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) |
27 |
|
relssres |
⊢ ( ( Rel ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ∧ dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) |
28 |
2 26 27
|
sylancr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) |
29 |
|
dvfg |
⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) : dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⟶ ℂ ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) : dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⟶ ℂ ) |
31 |
30
|
ffund |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → Fun ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) |
32 |
|
ssidd |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ℂ ⊆ ℂ ) |
33 |
1
|
cnfldtopon |
⊢ 𝐽 ∈ ( TopOn ‘ ℂ ) |
34 |
|
simprl |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → 𝐴 ∈ 𝐽 ) |
35 |
|
toponss |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ ℂ ) |
36 |
33 34 35
|
sylancr |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → 𝐴 ⊆ ℂ ) |
37 |
|
dvres2 |
⊢ ( ( ( ℂ ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ ℂ ) ) → ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) |
38 |
32 5 36 4 37
|
syl22anc |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) |
39 |
|
funssres |
⊢ ( ( Fun ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ∧ ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) |
40 |
31 38 39
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) |
41 |
28 40
|
eqtr3d |
⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) |