Metamath Proof Explorer

Theorem dvsubf

Description: The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvsubf.s 
|- ( ph -> S e. { RR , CC } )
dvsubf.f 
|- ( ph -> F : X --> CC )
dvsubf.g 
|- ( ph -> G : X --> CC )
dvsubf.fdv 
|- ( ph -> dom ( S _D F ) = X )
dvsubf.gdv 
|- ( ph -> dom ( S _D G ) = X )
Assertion dvsubf 
|- ( ph -> ( S _D ( F oF - G ) ) = ( ( S _D F ) oF - ( S _D G ) ) )

Proof

Step Hyp Ref Expression
1 dvsubf.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvsubf.f 
 |-  ( ph -> F : X --> CC )
3 dvsubf.g 
 |-  ( ph -> G : X --> CC )
4 dvsubf.fdv 
 |-  ( ph -> dom ( S _D F ) = X )
5 dvsubf.gdv 
 |-  ( ph -> dom ( S _D G ) = X )
6 2 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
7 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
8 1 7 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
9 4 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
10 8 9 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
11 10 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. CC )
12 2 feqmptd 
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
13 12 oveq2d 
 |-  ( ph -> ( S _D F ) = ( S _D ( x e. X |-> ( F ` x ) ) ) )
14 10 feqmptd 
 |-  ( ph -> ( S _D F ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )
15 13 14 eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> ( F ` x ) ) ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )
16 3 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
17 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
18 1 17 syl 
 |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )
19 5 feq2d 
 |-  ( ph -> ( ( S _D G ) : dom ( S _D G ) --> CC <-> ( S _D G ) : X --> CC ) )
20 18 19 mpbid 
 |-  ( ph -> ( S _D G ) : X --> CC )
21 20 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) e. CC )
22 3 feqmptd 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
23 22 oveq2d 
 |-  ( ph -> ( S _D G ) = ( S _D ( x e. X |-> ( G ` x ) ) ) )
24 20 feqmptd 
 |-  ( ph -> ( S _D G ) = ( x e. X |-> ( ( S _D G ) ` x ) ) )
25 23 24 eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> ( G ` x ) ) ) = ( x e. X |-> ( ( S _D G ) ` x ) ) )
26 1 6 11 15 16 21 25 dvmptsub 
 |-  ( ph -> ( S _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) = ( x e. X |-> ( ( ( S _D F ) ` x ) - ( ( S _D G ) ` x ) ) ) )
27 ovex 
 |-  ( S _D F ) e. _V
28 27 dmex 
 |-  dom ( S _D F ) e. _V
29 4 28 eqeltrrdi 
 |-  ( ph -> X e. _V )
30 29 6 16 12 22 offval2 
 |-  ( ph -> ( F oF - G ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) )
31 30 oveq2d 
 |-  ( ph -> ( S _D ( F oF - G ) ) = ( S _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) )
32 29 11 21 14 24 offval2 
 |-  ( ph -> ( ( S _D F ) oF - ( S _D G ) ) = ( x e. X |-> ( ( ( S _D F ) ` x ) - ( ( S _D G ) ` x ) ) ) )
33 26 31 32 3eqtr4d 
 |-  ( ph -> ( S _D ( F oF - G ) ) = ( ( S _D F ) oF - ( S _D G ) ) )