Metamath Proof Explorer

Theorem dvcmul

Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvcmul.s 
|- ( ph -> S e. { RR , CC } )
dvcmul.f 
|- ( ph -> F : X --> CC )
dvcmul.a 
|- ( ph -> A e. CC )
dvcmul.x 
|- ( ph -> X C_ S )
dvcmul.c 
|- ( ph -> C e. dom ( S _D F ) )
Assertion dvcmul 
|- ( ph -> ( ( S _D ( ( S X. { A } ) oF x. F ) ) ` C ) = ( A x. ( ( S _D F ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 dvcmul.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvcmul.f 
 |-  ( ph -> F : X --> CC )
3 dvcmul.a 
 |-  ( ph -> A e. CC )
4 dvcmul.x 
 |-  ( ph -> X C_ S )
5 dvcmul.c 
 |-  ( ph -> C e. dom ( S _D F ) )
6 fconst6g 
 |-  ( A e. CC -> ( S X. { A } ) : S --> CC )
7 3 6 syl 
 |-  ( ph -> ( S X. { A } ) : S --> CC )
8 ssidd 
 |-  ( ph -> S C_ S )
9 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
10 1 9 syl 
 |-  ( ph -> S C_ CC )
11 10 2 4 dvbss 
 |-  ( ph -> dom ( S _D F ) C_ X )
12 11 5 sseldd 
 |-  ( ph -> C e. X )
13 4 12 sseldd 
 |-  ( ph -> C e. S )
14 fconst6g 
 |-  ( A e. CC -> ( CC X. { A } ) : CC --> CC )
15 3 14 syl 
 |-  ( ph -> ( CC X. { A } ) : CC --> CC )
16 ssidd 
 |-  ( ph -> CC C_ CC )
17 dvconst 
 |-  ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
18 3 17 syl 
 |-  ( ph -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
19 18 dmeqd 
 |-  ( ph -> dom ( CC _D ( CC X. { A } ) ) = dom ( CC X. { 0 } ) )
20 c0ex 
 |-  0 e. _V
21 20 fconst 
 |-  ( CC X. { 0 } ) : CC --> { 0 }
22 21 fdmi 
 |-  dom ( CC X. { 0 } ) = CC
23 19 22 eqtrdi 
 |-  ( ph -> dom ( CC _D ( CC X. { A } ) ) = CC )
24 10 23 sseqtrrd 
 |-  ( ph -> S C_ dom ( CC _D ( CC X. { A } ) ) )
25 dvres3 
 |-  ( ( ( S e. { RR , CC } /\ ( CC X. { A } ) : CC --> CC ) /\ ( CC C_ CC /\ S C_ dom ( CC _D ( CC X. { A } ) ) ) ) -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( ( CC _D ( CC X. { A } ) ) |` S ) )
26 1 15 16 24 25 syl22anc 
 |-  ( ph -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( ( CC _D ( CC X. { A } ) ) |` S ) )
27 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
28 10 27 syl 
 |-  ( ph -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
29 28 oveq2d 
 |-  ( ph -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( S _D ( S X. { A } ) ) )
30 18 reseq1d 
 |-  ( ph -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( ( CC X. { 0 } ) |` S ) )
31 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
32 10 31 syl 
 |-  ( ph -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
33 30 32 eqtrd 
 |-  ( ph -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( S X. { 0 } ) )
34 26 29 33 3eqtr3d 
 |-  ( ph -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )
35 20 fconst2 
 |-  ( ( S _D ( S X. { A } ) ) : S --> { 0 } <-> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )
36 34 35 sylibr 
 |-  ( ph -> ( S _D ( S X. { A } ) ) : S --> { 0 } )
37 36 fdmd 
 |-  ( ph -> dom ( S _D ( S X. { A } ) ) = S )
38 13 37 eleqtrrd 
 |-  ( ph -> C e. dom ( S _D ( S X. { A } ) ) )
39 7 8 2 4 1 38 5 dvmul 
 |-  ( ph -> ( ( S _D ( ( S X. { A } ) oF x. F ) ) ` C ) = ( ( ( ( S _D ( S X. { A } ) ) ` C ) x. ( F ` C ) ) + ( ( ( S _D F ) ` C ) x. ( ( S X. { A } ) ` C ) ) ) )
40 34 fveq1d 
 |-  ( ph -> ( ( S _D ( S X. { A } ) ) ` C ) = ( ( S X. { 0 } ) ` C ) )
41 20 fvconst2 
 |-  ( C e. S -> ( ( S X. { 0 } ) ` C ) = 0 )
42 13 41 syl 
 |-  ( ph -> ( ( S X. { 0 } ) ` C ) = 0 )
43 40 42 eqtrd 
 |-  ( ph -> ( ( S _D ( S X. { A } ) ) ` C ) = 0 )
44 43 oveq1d 
 |-  ( ph -> ( ( ( S _D ( S X. { A } ) ) ` C ) x. ( F ` C ) ) = ( 0 x. ( F ` C ) ) )
45 2 12 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. CC )
46 45 mul02d 
 |-  ( ph -> ( 0 x. ( F ` C ) ) = 0 )
47 44 46 eqtrd 
 |-  ( ph -> ( ( ( S _D ( S X. { A } ) ) ` C ) x. ( F ` C ) ) = 0 )
48 fvconst2g 
 |-  ( ( A e. CC /\ C e. S ) -> ( ( S X. { A } ) ` C ) = A )
49 3 13 48 syl2anc 
 |-  ( ph -> ( ( S X. { A } ) ` C ) = A )
50 49 oveq2d 
 |-  ( ph -> ( ( ( S _D F ) ` C ) x. ( ( S X. { A } ) ` C ) ) = ( ( ( S _D F ) ` C ) x. A ) )
51 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
52 1 51 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
53 52 5 ffvelcdmd 
 |-  ( ph -> ( ( S _D F ) ` C ) e. CC )
54 53 3 mulcomd 
 |-  ( ph -> ( ( ( S _D F ) ` C ) x. A ) = ( A x. ( ( S _D F ) ` C ) ) )
55 50 54 eqtrd 
 |-  ( ph -> ( ( ( S _D F ) ` C ) x. ( ( S X. { A } ) ` C ) ) = ( A x. ( ( S _D F ) ` C ) ) )
56 47 55 oveq12d 
 |-  ( ph -> ( ( ( ( S _D ( S X. { A } ) ) ` C ) x. ( F ` C ) ) + ( ( ( S _D F ) ` C ) x. ( ( S X. { A } ) ` C ) ) ) = ( 0 + ( A x. ( ( S _D F ) ` C ) ) ) )
57 3 53 mulcld 
 |-  ( ph -> ( A x. ( ( S _D F ) ` C ) ) e. CC )
58 57 addlidd 
 |-  ( ph -> ( 0 + ( A x. ( ( S _D F ) ` C ) ) ) = ( A x. ( ( S _D F ) ` C ) ) )
59 39 56 58 3eqtrd 
 |-  ( ph -> ( ( S _D ( ( S X. { A } ) oF x. F ) ) ` C ) = ( A x. ( ( S _D F ) ` C ) ) )