Metamath Proof Explorer

Theorem dvres3a

Description: Restriction of a complex differentiable function to the reals. This version of dvres3 assumes that F is differentiable on its domain, but does not require F to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis dvres3a.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dvres3a ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ∈ 𝐽 ∧ dom ( ℂ D 𝐹 ) = 𝐴 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )

Proof

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 𝐹 ) ↾ 𝑆 ) )