Metamath Proof Explorer

Theorem dvmptmulf

Description: Function-builder for derivative, product rule. A version of dvmptmul using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptmulf.ph 
|- F/ x ph
dvmptmulf.s 
|- ( ph -> S e. { RR , CC } )
dvmptmulf.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptmulf.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptmulf.ab 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
dvmptmulf.c 
|- ( ( ph /\ x e. X ) -> C e. CC )
dvmptmulf.d 
|- ( ( ph /\ x e. X ) -> D e. W )
dvmptmulf.cd 
|- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
Assertion dvmptmulf 
|- ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 dvmptmulf.ph 
 |-  F/ x ph
2 dvmptmulf.s 
 |-  ( ph -> S e. { RR , CC } )
3 dvmptmulf.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
4 dvmptmulf.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
5 dvmptmulf.ab 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
6 dvmptmulf.c 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
7 dvmptmulf.d 
 |-  ( ( ph /\ x e. X ) -> D e. W )
8 dvmptmulf.cd 
 |-  ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
9 nfcv 
 |-  F/_ y ( A x. C )
10 nfcsb1v 
 |-  F/_ x [_ y / x ]_ A
11 nfcv 
 |-  F/_ x x.
12 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
13 10 11 12 nfov 
 |-  F/_ x ( [_ y / x ]_ A x. [_ y / x ]_ C )
14 csbeq1a 
 |-  ( x = y -> A = [_ y / x ]_ A )
15 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
16 14 15 oveq12d 
 |-  ( x = y -> ( A x. C ) = ( [_ y / x ]_ A x. [_ y / x ]_ C ) )
17 9 13 16 cbvmpt 
 |-  ( x e. X |-> ( A x. C ) ) = ( y e. X |-> ( [_ y / x ]_ A x. [_ y / x ]_ C ) )
18 17 oveq2i 
 |-  ( S _D ( x e. X |-> ( A x. C ) ) ) = ( S _D ( y e. X |-> ( [_ y / x ]_ A x. [_ y / x ]_ C ) ) )
19 18 a1i 
 |-  ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( S _D ( y e. X |-> ( [_ y / x ]_ A x. [_ y / x ]_ C ) ) ) )
20 nfv 
 |-  F/ x y e. X
21 1 20 nfan 
 |-  F/ x ( ph /\ y e. X )
22 10 nfel1 
 |-  F/ x [_ y / x ]_ A e. CC
23 21 22 nfim 
 |-  F/ x ( ( ph /\ y e. X ) -> [_ y / x ]_ A e. CC )
24 eleq1w 
 |-  ( x = y -> ( x e. X <-> y e. X ) )
25 24 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. X ) <-> ( ph /\ y e. X ) ) )
26 14 eleq1d 
 |-  ( x = y -> ( A e. CC <-> [_ y / x ]_ A e. CC ) )
27 25 26 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. X ) -> A e. CC ) <-> ( ( ph /\ y e. X ) -> [_ y / x ]_ A e. CC ) ) )
28 23 27 3 chvarfv 
 |-  ( ( ph /\ y e. X ) -> [_ y / x ]_ A e. CC )
29 nfcv 
 |-  F/_ x y
30 29 nfcsb1 
 |-  F/_ x [_ y / x ]_ B
31 nfcv 
 |-  F/_ x V
32 30 31 nfel 
 |-  F/ x [_ y / x ]_ B e. V
33 21 32 nfim 
 |-  F/ x ( ( ph /\ y e. X ) -> [_ y / x ]_ B e. V )
34 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
35 34 eleq1d 
 |-  ( x = y -> ( B e. V <-> [_ y / x ]_ B e. V ) )
36 25 35 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. X ) -> B e. V ) <-> ( ( ph /\ y e. X ) -> [_ y / x ]_ B e. V ) ) )
37 33 36 4 chvarfv 
 |-  ( ( ph /\ y e. X ) -> [_ y / x ]_ B e. V )
38 nfcv 
 |-  F/_ y A
39 csbeq1a 
 |-  ( y = x -> [_ y / x ]_ A = [_ x / y ]_ [_ y / x ]_ A )
40 csbcow 
 |-  [_ x / y ]_ [_ y / x ]_ A = [_ x / x ]_ A
41 csbid 
 |-  [_ x / x ]_ A = A
42 40 41 eqtri 
 |-  [_ x / y ]_ [_ y / x ]_ A = A
43 42 a1i 
 |-  ( y = x -> [_ x / y ]_ [_ y / x ]_ A = A )
44 39 43 eqtrd 
 |-  ( y = x -> [_ y / x ]_ A = A )
45 10 38 44 cbvmpt 
 |-  ( y e. X |-> [_ y / x ]_ A ) = ( x e. X |-> A )
46 45 oveq2i 
 |-  ( S _D ( y e. X |-> [_ y / x ]_ A ) ) = ( S _D ( x e. X |-> A ) )
47 46 a1i 
 |-  ( ph -> ( S _D ( y e. X |-> [_ y / x ]_ A ) ) = ( S _D ( x e. X |-> A ) ) )
48 nfcv 
 |-  F/_ y B
49 48 30 34 cbvmpt 
 |-  ( x e. X |-> B ) = ( y e. X |-> [_ y / x ]_ B )
50 49 a1i 
 |-  ( ph -> ( x e. X |-> B ) = ( y e. X |-> [_ y / x ]_ B ) )
51 47 5 50 3eqtrd 
 |-  ( ph -> ( S _D ( y e. X |-> [_ y / x ]_ A ) ) = ( y e. X |-> [_ y / x ]_ B ) )
52 12 nfel1 
 |-  F/ x [_ y / x ]_ C e. CC
53 21 52 nfim 
 |-  F/ x ( ( ph /\ y e. X ) -> [_ y / x ]_ C e. CC )
54 15 eleq1d 
 |-  ( x = y -> ( C e. CC <-> [_ y / x ]_ C e. CC ) )
55 25 54 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. X ) -> C e. CC ) <-> ( ( ph /\ y e. X ) -> [_ y / x ]_ C e. CC ) ) )
56 53 55 6 chvarfv 
 |-  ( ( ph /\ y e. X ) -> [_ y / x ]_ C e. CC )
57 29 nfcsb1 
 |-  F/_ x [_ y / x ]_ D
58 nfcv 
 |-  F/_ x W
59 57 58 nfel 
 |-  F/ x [_ y / x ]_ D e. W
60 21 59 nfim 
 |-  F/ x ( ( ph /\ y e. X ) -> [_ y / x ]_ D e. W )
61 csbeq1a 
 |-  ( x = y -> D = [_ y / x ]_ D )
62 61 eleq1d 
 |-  ( x = y -> ( D e. W <-> [_ y / x ]_ D e. W ) )
63 25 62 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. X ) -> D e. W ) <-> ( ( ph /\ y e. X ) -> [_ y / x ]_ D e. W ) ) )
64 60 63 7 chvarfv 
 |-  ( ( ph /\ y e. X ) -> [_ y / x ]_ D e. W )
65 nfcv 
 |-  F/_ y C
66 eqcom 
 |-  ( x = y <-> y = x )
67 66 imbi1i 
 |-  ( ( x = y -> C = [_ y / x ]_ C ) <-> ( y = x -> C = [_ y / x ]_ C ) )
68 eqcom 
 |-  ( C = [_ y / x ]_ C <-> [_ y / x ]_ C = C )
69 68 imbi2i 
 |-  ( ( y = x -> C = [_ y / x ]_ C ) <-> ( y = x -> [_ y / x ]_ C = C ) )
70 67 69 bitri 
 |-  ( ( x = y -> C = [_ y / x ]_ C ) <-> ( y = x -> [_ y / x ]_ C = C ) )
71 15 70 mpbi 
 |-  ( y = x -> [_ y / x ]_ C = C )
72 12 65 71 cbvmpt 
 |-  ( y e. X |-> [_ y / x ]_ C ) = ( x e. X |-> C )
73 72 oveq2i 
 |-  ( S _D ( y e. X |-> [_ y / x ]_ C ) ) = ( S _D ( x e. X |-> C ) )
74 73 a1i 
 |-  ( ph -> ( S _D ( y e. X |-> [_ y / x ]_ C ) ) = ( S _D ( x e. X |-> C ) ) )
75 nfcv 
 |-  F/_ y D
76 75 57 61 cbvmpt 
 |-  ( x e. X |-> D ) = ( y e. X |-> [_ y / x ]_ D )
77 76 a1i 
 |-  ( ph -> ( x e. X |-> D ) = ( y e. X |-> [_ y / x ]_ D ) )
78 74 8 77 3eqtrd 
 |-  ( ph -> ( S _D ( y e. X |-> [_ y / x ]_ C ) ) = ( y e. X |-> [_ y / x ]_ D ) )
79 2 28 37 51 56 64 78 dvmptmul 
 |-  ( ph -> ( S _D ( y e. X |-> ( [_ y / x ]_ A x. [_ y / x ]_ C ) ) ) = ( y e. X |-> ( ( [_ y / x ]_ B x. [_ y / x ]_ C ) + ( [_ y / x ]_ D x. [_ y / x ]_ A ) ) ) )
80 30 11 12 nfov 
 |-  F/_ x ( [_ y / x ]_ B x. [_ y / x ]_ C )
81 nfcv 
 |-  F/_ x +
82 57 11 10 nfov 
 |-  F/_ x ( [_ y / x ]_ D x. [_ y / x ]_ A )
83 80 81 82 nfov 
 |-  F/_ x ( ( [_ y / x ]_ B x. [_ y / x ]_ C ) + ( [_ y / x ]_ D x. [_ y / x ]_ A ) )
84 nfcv 
 |-  F/_ y ( ( B x. C ) + ( D x. A ) )
85 66 imbi1i 
 |-  ( ( x = y -> B = [_ y / x ]_ B ) <-> ( y = x -> B = [_ y / x ]_ B ) )
86 eqcom 
 |-  ( B = [_ y / x ]_ B <-> [_ y / x ]_ B = B )
87 86 imbi2i 
 |-  ( ( y = x -> B = [_ y / x ]_ B ) <-> ( y = x -> [_ y / x ]_ B = B ) )
88 85 87 bitri 
 |-  ( ( x = y -> B = [_ y / x ]_ B ) <-> ( y = x -> [_ y / x ]_ B = B ) )
89 34 88 mpbi 
 |-  ( y = x -> [_ y / x ]_ B = B )
90 89 71 oveq12d 
 |-  ( y = x -> ( [_ y / x ]_ B x. [_ y / x ]_ C ) = ( B x. C ) )
91 66 imbi1i 
 |-  ( ( x = y -> D = [_ y / x ]_ D ) <-> ( y = x -> D = [_ y / x ]_ D ) )
92 eqcom 
 |-  ( D = [_ y / x ]_ D <-> [_ y / x ]_ D = D )
93 92 imbi2i 
 |-  ( ( y = x -> D = [_ y / x ]_ D ) <-> ( y = x -> [_ y / x ]_ D = D ) )
94 91 93 bitri 
 |-  ( ( x = y -> D = [_ y / x ]_ D ) <-> ( y = x -> [_ y / x ]_ D = D ) )
95 61 94 mpbi 
 |-  ( y = x -> [_ y / x ]_ D = D )
96 95 44 oveq12d 
 |-  ( y = x -> ( [_ y / x ]_ D x. [_ y / x ]_ A ) = ( D x. A ) )
97 90 96 oveq12d 
 |-  ( y = x -> ( ( [_ y / x ]_ B x. [_ y / x ]_ C ) + ( [_ y / x ]_ D x. [_ y / x ]_ A ) ) = ( ( B x. C ) + ( D x. A ) ) )
98 83 84 97 cbvmpt 
 |-  ( y e. X |-> ( ( [_ y / x ]_ B x. [_ y / x ]_ C ) + ( [_ y / x ]_ D x. [_ y / x ]_ A ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) )
99 98 a1i 
 |-  ( ph -> ( y e. X |-> ( ( [_ y / x ]_ B x. [_ y / x ]_ C ) + ( [_ y / x ]_ D x. [_ y / x ]_ A ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )
100 19 79 99 3eqtrd 
 |-  ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )