Metamath Proof Explorer

Theorem dvres3

Description: Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvres3 
|- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )

Proof

Step Hyp Ref Expression
1 reldv 
 |-  Rel ( S _D ( F |` S ) )
2 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
3 2 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> S C_ CC )
4 simplr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> F : A --> CC )
5 simprr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> S C_ dom ( CC _D F ) )
6 ssidd 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> CC C_ CC )
7 simprl 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> A C_ CC )
8 6 4 7 dvbss 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> dom ( CC _D F ) C_ A )
9 5 8 sstrd 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> S C_ A )
10 4 9 fssresd 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( F |` S ) : S --> CC )
11 ssidd 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> S C_ S )
12 3 10 11 dvbss 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> dom ( S _D ( F |` S ) ) C_ S )
13 ssdmres 
 |-  ( S C_ dom ( CC _D F ) <-> dom ( ( CC _D F ) |` S ) = S )
14 5 13 sylib 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> dom ( ( CC _D F ) |` S ) = S )
15 12 14 sseqtrrd 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> dom ( S _D ( F |` S ) ) C_ dom ( ( CC _D F ) |` S ) )
16 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 ) ) )
17 1 15 16 sylancr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( ( S _D ( F |` S ) ) |` dom ( ( CC _D F ) |` S ) ) = ( S _D ( F |` S ) ) )
18 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( F |` S ) ) : dom ( S _D ( F |` S ) ) --> CC )
19 18 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( S _D ( F |` S ) ) : dom ( S _D ( F |` S ) ) --> CC )
20 19 ffund 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> Fun ( S _D ( F |` S ) ) )
21 dvres2 
 |-  ( ( ( CC C_ CC /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ CC ) ) -> ( ( CC _D F ) |` S ) C_ ( S _D ( F |` S ) ) )
22 6 4 7 3 21 syl22anc 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( ( CC _D F ) |` S ) C_ ( S _D ( F |` S ) ) )
23 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 ) )
24 20 22 23 syl2anc 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( ( S _D ( F |` S ) ) |` dom ( ( CC _D F ) |` S ) ) = ( ( CC _D F ) |` S ) )
25 17 24 eqtr3d 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )