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 J = TopOpen fld
Assertion dvres3a S F : A A J dom F = A S D F S = F S

Proof

Step Hyp Ref Expression
1 dvres3a.j J = TopOpen fld
2 reldv Rel F S S
3 recnprss S S
4 3 ad2antrr S F : A A J dom F = A S
5 simplr S F : A A J dom F = A F : A
6 inss2 S A A
7 fssres F : A S A A F S A : S A
8 5 6 7 sylancl S F : A A J dom F = A F S A : S A
9 rescom F A S = F S A
10 resres F S A = F S A
11 9 10 eqtri F A S = F S A
12 ffn F : A F Fn A
13 fnresdm F Fn A F A = F
14 5 12 13 3syl S F : A A J dom F = A F A = F
15 14 reseq1d S F : A A J dom F = A F A S = F S
16 11 15 eqtr3id S F : A A J dom F = A F S A = F S
17 16 feq1d S F : A A J dom F = A F S A : S A F S : S A
18 8 17 mpbid S F : A A J dom F = A F S : S A
19 inss1 S A S
20 19 a1i S F : A A J dom F = A S A S
21 4 18 20 dvbss S F : A A J dom F = A dom F S S S A
22 dmres dom F S = S dom F
23 simprr S F : A A J dom F = A dom F = A
24 23 ineq2d S F : A A J dom F = A S dom F = S A
25 22 24 syl5eq S F : A A J dom F = A dom F S = S A
26 21 25 sseqtrrd S F : A A J dom F = A dom F S S dom F S
27 relssres Rel F S S dom F S S dom F S F S S dom F S = S D F S
28 2 26 27 sylancr S F : A A J dom F = A F S S dom F S = S D F S
29 dvfg S F S S : dom F S S
30 29 ad2antrr S F : A A J dom F = A F S S : dom F S S
31 30 ffund S F : A A J dom F = A Fun F S S
32 ssidd S F : A A J dom F = A
33 1 cnfldtopon J TopOn
34 simprl S F : A A J dom F = A A J
35 toponss J TopOn A J A
36 33 34 35 sylancr S F : A A J dom F = A A
37 dvres2 F : A A S F S S D F S
38 32 5 36 4 37 syl22anc S F : A A J dom F = A F S S D F S
39 funssres Fun F S S F S S D F S F S S dom F S = F S
40 31 38 39 syl2anc S F : A A J dom F = A F S S dom F S = F S
41 28 40 eqtr3d S F : A A J dom F = A S D F S = F S