Metamath Proof Explorer

Theorem dvres2

Description: Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex-differentiable then it is also real-differentiable. Unlike dvres , there is no simple reverse relation relating real-differentiable functions to complex differentiability, and indeed there are functions like Re ( x ) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion dvres2 
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( S _D F ) |` B ) C_ ( B _D ( F |` B ) ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( ( S _D F ) |` B )
2 1 a1i 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> Rel ( ( S _D F ) |` B ) )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
5 eqid 
 |-  ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
6 simp1l 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> S C_ CC )
7 simp1r 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> F : A --> CC )
8 simp2l 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> A C_ S )
9 simp2r 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> B C_ S )
10 simp3r 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> x ( S _D F ) y )
11 6 7 8 dvcl 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) /\ x ( S _D F ) y ) -> y e. CC )
12 10 11 mpdan 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> y e. CC )
13 simp3l 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> x e. B )
14 3 4 5 6 7 8 9 12 10 13 dvres2lem 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) /\ ( x e. B /\ x ( S _D F ) y ) ) -> x ( B _D ( F |` B ) ) y )
15 14 3expia 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( x e. B /\ x ( S _D F ) y ) -> x ( B _D ( F |` B ) ) y ) )
16 vex 
 |-  y e. _V
17 16 brresi 
 |-  ( x ( ( S _D F ) |` B ) y <-> ( x e. B /\ x ( S _D F ) y ) )
18 df-br 
 |-  ( x ( ( S _D F ) |` B ) y <-> <. x , y >. e. ( ( S _D F ) |` B ) )
19 17 18 bitr3i 
 |-  ( ( x e. B /\ x ( S _D F ) y ) <-> <. x , y >. e. ( ( S _D F ) |` B ) )
20 df-br 
 |-  ( x ( B _D ( F |` B ) ) y <-> <. x , y >. e. ( B _D ( F |` B ) ) )
21 15 19 20 3imtr3g 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( <. x , y >. e. ( ( S _D F ) |` B ) -> <. x , y >. e. ( B _D ( F |` B ) ) ) )
22 2 21 relssdv 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( S _D F ) |` B ) C_ ( B _D ( F |` B ) ) )