Metamath Proof Explorer

Theorem dvmptdiv

Description: Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptdiv.s 
|- ( ph -> S e. { RR , CC } )
dvmptdiv.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptdiv.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptdiv.da 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
dvmptdiv.c 
|- ( ( ph /\ x e. X ) -> C e. ( CC \ { 0 } ) )
dvmptdiv.d 
|- ( ( ph /\ x e. X ) -> D e. CC )
dvmptdiv.dc 
|- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
Assertion dvmptdiv 
|- ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvmptdiv.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptdiv.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
3 dvmptdiv.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
4 dvmptdiv.da 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
5 dvmptdiv.c 
 |-  ( ( ph /\ x e. X ) -> C e. ( CC \ { 0 } ) )
6 dvmptdiv.d 
 |-  ( ( ph /\ x e. X ) -> D e. CC )
7 dvmptdiv.dc 
 |-  ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
8 5 eldifad 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
9 eldifsn 
 |-  ( C e. ( CC \ { 0 } ) <-> ( C e. CC /\ C =/= 0 ) )
10 5 9 sylib 
 |-  ( ( ph /\ x e. X ) -> ( C e. CC /\ C =/= 0 ) )
11 10 simprd 
 |-  ( ( ph /\ x e. X ) -> C =/= 0 )
12 2 8 11 divrecd 
 |-  ( ( ph /\ x e. X ) -> ( A / C ) = ( A x. ( 1 / C ) ) )
13 12 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A / C ) ) = ( x e. X |-> ( A x. ( 1 / C ) ) ) )
14 13 oveq2d 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( S _D ( x e. X |-> ( A x. ( 1 / C ) ) ) ) )
15 8 11 reccld 
 |-  ( ( ph /\ x e. X ) -> ( 1 / C ) e. CC )
16 1cnd 
 |-  ( ( ph /\ x e. X ) -> 1 e. CC )
17 16 6 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( 1 x. D ) e. CC )
18 8 sqcld 
 |-  ( ( ph /\ x e. X ) -> ( C ^ 2 ) e. CC )
19 11 neneqd 
 |-  ( ( ph /\ x e. X ) -> -. C = 0 )
20 sqeq0 
 |-  ( C e. CC -> ( ( C ^ 2 ) = 0 <-> C = 0 ) )
21 8 20 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( C ^ 2 ) = 0 <-> C = 0 ) )
22 19 21 mtbird 
 |-  ( ( ph /\ x e. X ) -> -. ( C ^ 2 ) = 0 )
23 22 neqned 
 |-  ( ( ph /\ x e. X ) -> ( C ^ 2 ) =/= 0 )
24 17 18 23 divcld 
 |-  ( ( ph /\ x e. X ) -> ( ( 1 x. D ) / ( C ^ 2 ) ) e. CC )
25 24 negcld 
 |-  ( ( ph /\ x e. X ) -> -u ( ( 1 x. D ) / ( C ^ 2 ) ) e. CC )
26 1cnd 
 |-  ( ph -> 1 e. CC )
27 1 26 5 6 7 dvrecg 
 |-  ( ph -> ( S _D ( x e. X |-> ( 1 / C ) ) ) = ( x e. X |-> -u ( ( 1 x. D ) / ( C ^ 2 ) ) ) )
28 1 2 3 4 15 25 27 dvmptmul 
 |-  ( ph -> ( S _D ( x e. X |-> ( A x. ( 1 / C ) ) ) ) = ( x e. X |-> ( ( B x. ( 1 / C ) ) + ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) ) ) )
29 1 2 3 4 dvmptcl 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
30 29 8 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( B x. C ) e. CC )
31 30 18 23 divcld 
 |-  ( ( ph /\ x e. X ) -> ( ( B x. C ) / ( C ^ 2 ) ) e. CC )
32 6 2 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( D x. A ) e. CC )
33 32 18 23 divcld 
 |-  ( ( ph /\ x e. X ) -> ( ( D x. A ) / ( C ^ 2 ) ) e. CC )
34 31 33 negsubd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( B x. C ) / ( C ^ 2 ) ) + -u ( ( D x. A ) / ( C ^ 2 ) ) ) = ( ( ( B x. C ) / ( C ^ 2 ) ) - ( ( D x. A ) / ( C ^ 2 ) ) ) )
35 29 16 8 11 div12d 
 |-  ( ( ph /\ x e. X ) -> ( B x. ( 1 / C ) ) = ( 1 x. ( B / C ) ) )
36 29 8 11 divcld 
 |-  ( ( ph /\ x e. X ) -> ( B / C ) e. CC )
37 36 mulid2d 
 |-  ( ( ph /\ x e. X ) -> ( 1 x. ( B / C ) ) = ( B / C ) )
38 8 sqvald 
 |-  ( ( ph /\ x e. X ) -> ( C ^ 2 ) = ( C x. C ) )
39 38 oveq2d 
 |-  ( ( ph /\ x e. X ) -> ( ( B x. C ) / ( C ^ 2 ) ) = ( ( B x. C ) / ( C x. C ) ) )
40 29 8 8 11 11 divcan5rd 
 |-  ( ( ph /\ x e. X ) -> ( ( B x. C ) / ( C x. C ) ) = ( B / C ) )
41 39 40 eqtr2d 
 |-  ( ( ph /\ x e. X ) -> ( B / C ) = ( ( B x. C ) / ( C ^ 2 ) ) )
42 35 37 41 3eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( B x. ( 1 / C ) ) = ( ( B x. C ) / ( C ^ 2 ) ) )
43 6 mulid2d 
 |-  ( ( ph /\ x e. X ) -> ( 1 x. D ) = D )
44 43 oveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( 1 x. D ) / ( C ^ 2 ) ) = ( D / ( C ^ 2 ) ) )
45 44 negeqd 
 |-  ( ( ph /\ x e. X ) -> -u ( ( 1 x. D ) / ( C ^ 2 ) ) = -u ( D / ( C ^ 2 ) ) )
46 45 oveq1d 
 |-  ( ( ph /\ x e. X ) -> ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) = ( -u ( D / ( C ^ 2 ) ) x. A ) )
47 6 18 23 divcld 
 |-  ( ( ph /\ x e. X ) -> ( D / ( C ^ 2 ) ) e. CC )
48 47 2 mulneg1d 
 |-  ( ( ph /\ x e. X ) -> ( -u ( D / ( C ^ 2 ) ) x. A ) = -u ( ( D / ( C ^ 2 ) ) x. A ) )
49 6 2 18 23 div23d 
 |-  ( ( ph /\ x e. X ) -> ( ( D x. A ) / ( C ^ 2 ) ) = ( ( D / ( C ^ 2 ) ) x. A ) )
50 49 eqcomd 
 |-  ( ( ph /\ x e. X ) -> ( ( D / ( C ^ 2 ) ) x. A ) = ( ( D x. A ) / ( C ^ 2 ) ) )
51 50 negeqd 
 |-  ( ( ph /\ x e. X ) -> -u ( ( D / ( C ^ 2 ) ) x. A ) = -u ( ( D x. A ) / ( C ^ 2 ) ) )
52 46 48 51 3eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) = -u ( ( D x. A ) / ( C ^ 2 ) ) )
53 42 52 oveq12d 
 |-  ( ( ph /\ x e. X ) -> ( ( B x. ( 1 / C ) ) + ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) ) = ( ( ( B x. C ) / ( C ^ 2 ) ) + -u ( ( D x. A ) / ( C ^ 2 ) ) ) )
54 30 32 18 23 divsubdird 
 |-  ( ( ph /\ x e. X ) -> ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) = ( ( ( B x. C ) / ( C ^ 2 ) ) - ( ( D x. A ) / ( C ^ 2 ) ) ) )
55 34 53 54 3eqtr4d 
 |-  ( ( ph /\ x e. X ) -> ( ( B x. ( 1 / C ) ) + ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) ) = ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) )
56 55 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( B x. ( 1 / C ) ) + ( -u ( ( 1 x. D ) / ( C ^ 2 ) ) x. A ) ) ) = ( x e. X |-> ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) ) )
57 14 28 56 3eqtrd 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) ) )