Metamath Proof Explorer

Theorem dvdivf

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

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

Proof

Step Hyp Ref Expression
1 dvdivf.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvdivf.f 
 |-  ( ph -> F : X --> CC )
3 dvdivf.g 
 |-  ( ph -> G : X --> ( CC \ { 0 } ) )
4 dvdivf.fdv 
 |-  ( ph -> dom ( S _D F ) = X )
5 dvdivf.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 \ { 0 } ) )
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 dvmptdiv 
 |-  ( ph -> ( S _D ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) ) = ( x e. X |-> ( ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) / ( ( G ` x ) ^ 2 ) ) ) )
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 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) e. _V )
33 16 eldifad 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
34 33 sqcld 
 |-  ( ( ph /\ x e. X ) -> ( ( G ` x ) ^ 2 ) e. CC )
35 11 33 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) e. CC )
36 21 6 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) e. CC )
37 29 11 33 14 22 offval2 
 |-  ( ph -> ( ( S _D F ) oF x. G ) = ( x e. X |-> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) ) )
38 29 21 6 24 12 offval2 
 |-  ( ph -> ( ( S _D G ) oF x. F ) = ( x e. X |-> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )
39 29 35 36 37 38 offval2 
 |-  ( ph -> ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) = ( x e. X |-> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) ) )
40 29 16 16 22 22 offval2 
 |-  ( ph -> ( G oF x. G ) = ( x e. X |-> ( ( G ` x ) x. ( G ` x ) ) ) )
41 33 sqvald 
 |-  ( ( ph /\ x e. X ) -> ( ( G ` x ) ^ 2 ) = ( ( G ` x ) x. ( G ` x ) ) )
42 41 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( G ` x ) ^ 2 ) ) = ( x e. X |-> ( ( G ` x ) x. ( G ` x ) ) ) )
43 40 42 eqtr4d 
 |-  ( ph -> ( G oF x. G ) = ( x e. X |-> ( ( G ` x ) ^ 2 ) ) )
44 29 32 34 39 43 offval2 
 |-  ( ph -> ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) = ( x e. X |-> ( ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) / ( ( G ` x ) ^ 2 ) ) ) )
45 26 31 44 3eqtr4d 
 |-  ( ph -> ( S _D ( F oF / G ) ) = ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) )