Metamath Proof Explorer

Theorem dvmptdivc

Description: Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvmptadd.s 
|- ( ph -> S e. { RR , CC } )
dvmptadd.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptadd.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptadd.da 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
dvmptcmul.c 
|- ( ph -> C e. CC )
dvmptdivc.0 
|- ( ph -> C =/= 0 )
Assertion dvmptdivc 
|- ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( B / C ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptadd.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
3 dvmptadd.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
4 dvmptadd.da 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
5 dvmptcmul.c 
 |-  ( ph -> C e. CC )
6 dvmptdivc.0 
 |-  ( ph -> C =/= 0 )
7 5 6 reccld 
 |-  ( ph -> ( 1 / C ) e. CC )
8 1 2 3 4 7 dvmptcmul 
 |-  ( ph -> ( S _D ( x e. X |-> ( ( 1 / C ) x. A ) ) ) = ( x e. X |-> ( ( 1 / C ) x. B ) ) )
9 5 adantr 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
10 6 adantr 
 |-  ( ( ph /\ x e. X ) -> C =/= 0 )
11 2 9 10 divrec2d 
 |-  ( ( ph /\ x e. X ) -> ( A / C ) = ( ( 1 / C ) x. A ) )
12 11 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A / C ) ) = ( x e. X |-> ( ( 1 / C ) x. A ) ) )
13 12 oveq2d 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( S _D ( x e. X |-> ( ( 1 / C ) x. A ) ) ) )
14 1 2 3 4 dvmptcl 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
15 14 9 10 divrec2d 
 |-  ( ( ph /\ x e. X ) -> ( B / C ) = ( ( 1 / C ) x. B ) )
16 15 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( B / C ) ) = ( x e. X |-> ( ( 1 / C ) x. B ) ) )
17 8 13 16 3eqtr4d 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( B / C ) ) )