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 eqtr3id ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴𝐽 ∧ 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 𝐹 ) ↾ 𝑆 ) )