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 ` CCfld )
Assertion dvres3a 
|- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A e. J /\ dom ( CC _D F ) = A ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )

Proof

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