Metamath Proof Explorer

Theorem dvcmulf

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 )
dvcmulf.df 
|- ( ph -> dom ( S _D F ) = X )
Assertion dvcmulf 
|- ( ph -> ( S _D ( ( S X. { A } ) oF x. F ) ) = ( ( S X. { A } ) oF x. ( S _D F ) ) )

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 dvcmulf.df 
 |-  ( ph -> dom ( S _D F ) = X )
5 fconstg 
 |-  ( A e. CC -> ( X X. { A } ) : X --> { A } )
6 3 5 syl 
 |-  ( ph -> ( X X. { A } ) : X --> { A } )
7 3 snssd 
 |-  ( ph -> { A } C_ CC )
8 6 7 fssd 
 |-  ( ph -> ( X X. { A } ) : X --> CC )
9 c0ex 
 |-  0 e. _V
10 9 fconst 
 |-  ( X X. { 0 } ) : X --> { 0 }
11 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
12 1 11 syl 
 |-  ( ph -> S C_ CC )
13 fconstg 
 |-  ( A e. CC -> ( S X. { A } ) : S --> { A } )
14 3 13 syl 
 |-  ( ph -> ( S X. { A } ) : S --> { A } )
15 14 7 fssd 
 |-  ( ph -> ( S X. { A } ) : S --> CC )
16 ssidd 
 |-  ( ph -> S C_ S )
17 dvbsss 
 |-  dom ( S _D F ) C_ S
18 17 a1i 
 |-  ( ph -> dom ( S _D F ) C_ S )
19 4 18 eqsstrrd 
 |-  ( ph -> X C_ S )
20 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
21 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
22 20 21 dvres 
 |-  ( ( ( S C_ CC /\ ( S X. { A } ) : S --> CC ) /\ ( S C_ S /\ X C_ S ) ) -> ( S _D ( ( S X. { A } ) |` X ) ) = ( ( S _D ( S X. { A } ) ) |` ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) ) )
23 12 15 16 19 22 syl22anc 
 |-  ( ph -> ( S _D ( ( S X. { A } ) |` X ) ) = ( ( S _D ( S X. { A } ) ) |` ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) ) )
24 19 resmptd 
 |-  ( ph -> ( ( x e. S |-> A ) |` X ) = ( x e. X |-> A ) )
25 fconstmpt 
 |-  ( S X. { A } ) = ( x e. S |-> A )
26 25 reseq1i 
 |-  ( ( S X. { A } ) |` X ) = ( ( x e. S |-> A ) |` X )
27 fconstmpt 
 |-  ( X X. { A } ) = ( x e. X |-> A )
28 24 26 27 3eqtr4g 
 |-  ( ph -> ( ( S X. { A } ) |` X ) = ( X X. { A } ) )
29 28 oveq2d 
 |-  ( ph -> ( S _D ( ( S X. { A } ) |` X ) ) = ( S _D ( X X. { A } ) ) )
30 19 resmptd 
 |-  ( ph -> ( ( x e. S |-> 0 ) |` X ) = ( x e. X |-> 0 ) )
31 fconstg 
 |-  ( A e. CC -> ( CC X. { A } ) : CC --> { A } )
32 3 31 syl 
 |-  ( ph -> ( CC X. { A } ) : CC --> { A } )
33 32 7 fssd 
 |-  ( ph -> ( CC X. { A } ) : CC --> CC )
34 ssidd 
 |-  ( ph -> CC C_ CC )
35 dvconst 
 |-  ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
36 3 35 syl 
 |-  ( ph -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
37 36 dmeqd 
 |-  ( ph -> dom ( CC _D ( CC X. { A } ) ) = dom ( CC X. { 0 } ) )
38 9 fconst 
 |-  ( CC X. { 0 } ) : CC --> { 0 }
39 38 fdmi 
 |-  dom ( CC X. { 0 } ) = CC
40 37 39 eqtrdi 
 |-  ( ph -> dom ( CC _D ( CC X. { A } ) ) = CC )
41 12 40 sseqtrrd 
 |-  ( ph -> S C_ dom ( CC _D ( CC X. { A } ) ) )
42 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 ) )
43 1 33 34 41 42 syl22anc 
 |-  ( ph -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( ( CC _D ( CC X. { A } ) ) |` S ) )
44 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
45 12 44 syl 
 |-  ( ph -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
46 45 oveq2d 
 |-  ( ph -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( S _D ( S X. { A } ) ) )
47 36 reseq1d 
 |-  ( ph -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( ( CC X. { 0 } ) |` S ) )
48 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
49 12 48 syl 
 |-  ( ph -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
50 47 49 eqtrd 
 |-  ( ph -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( S X. { 0 } ) )
51 43 46 50 3eqtr3d 
 |-  ( ph -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )
52 fconstmpt 
 |-  ( S X. { 0 } ) = ( x e. S |-> 0 )
53 51 52 eqtrdi 
 |-  ( ph -> ( S _D ( S X. { A } ) ) = ( x e. S |-> 0 ) )
54 20 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
55 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
56 54 12 55 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
57 topontop 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
58 56 57 syl 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
59 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
60 56 59 syl 
 |-  ( ph -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
61 19 60 sseqtrd 
 |-  ( ph -> X C_ U. ( ( TopOpen ` CCfld ) |`t S ) )
62 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t S ) = U. ( ( TopOpen ` CCfld ) |`t S )
63 62 ntrss2 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ X C_ U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) C_ X )
64 58 61 63 syl2anc 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) C_ X )
65 12 2 19 21 20 dvbssntr 
 |-  ( ph -> dom ( S _D F ) C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
66 4 65 eqsstrrd 
 |-  ( ph -> X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
67 64 66 eqssd 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) = X )
68 53 67 reseq12d 
 |-  ( ph -> ( ( S _D ( S X. { A } ) ) |` ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) ) = ( ( x e. S |-> 0 ) |` X ) )
69 fconstmpt 
 |-  ( X X. { 0 } ) = ( x e. X |-> 0 )
70 69 a1i 
 |-  ( ph -> ( X X. { 0 } ) = ( x e. X |-> 0 ) )
71 30 68 70 3eqtr4d 
 |-  ( ph -> ( ( S _D ( S X. { A } ) ) |` ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) ) = ( X X. { 0 } ) )
72 23 29 71 3eqtr3d 
 |-  ( ph -> ( S _D ( X X. { A } ) ) = ( X X. { 0 } ) )
73 72 feq1d 
 |-  ( ph -> ( ( S _D ( X X. { A } ) ) : X --> { 0 } <-> ( X X. { 0 } ) : X --> { 0 } ) )
74 10 73 mpbiri 
 |-  ( ph -> ( S _D ( X X. { A } ) ) : X --> { 0 } )
75 74 fdmd 
 |-  ( ph -> dom ( S _D ( X X. { A } ) ) = X )
76 1 8 2 75 4 dvmulf 
 |-  ( ph -> ( S _D ( ( X X. { A } ) oF x. F ) ) = ( ( ( S _D ( X X. { A } ) ) oF x. F ) oF + ( ( S _D F ) oF x. ( X X. { A } ) ) ) )
77 sseqin2 
 |-  ( X C_ S <-> ( S i^i X ) = X )
78 19 77 sylib 
 |-  ( ph -> ( S i^i X ) = X )
79 78 mpteq1d 
 |-  ( ph -> ( x e. ( S i^i X ) |-> ( A x. ( F ` x ) ) ) = ( x e. X |-> ( A x. ( F ` x ) ) ) )
80 14 ffnd 
 |-  ( ph -> ( S X. { A } ) Fn S )
81 2 ffnd 
 |-  ( ph -> F Fn X )
82 1 19 ssexd 
 |-  ( ph -> X e. _V )
83 eqid 
 |-  ( S i^i X ) = ( S i^i X )
84 fvconst2g 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( S X. { A } ) ` x ) = A )
85 3 84 sylan 
 |-  ( ( ph /\ x e. S ) -> ( ( S X. { A } ) ` x ) = A )
86 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = ( F ` x ) )
87 80 81 1 82 83 85 86 offval 
 |-  ( ph -> ( ( S X. { A } ) oF x. F ) = ( x e. ( S i^i X ) |-> ( A x. ( F ` x ) ) ) )
88 6 ffnd 
 |-  ( ph -> ( X X. { A } ) Fn X )
89 inidm 
 |-  ( X i^i X ) = X
90 fvconst2g 
 |-  ( ( A e. CC /\ x e. X ) -> ( ( X X. { A } ) ` x ) = A )
91 3 90 sylan 
 |-  ( ( ph /\ x e. X ) -> ( ( X X. { A } ) ` x ) = A )
92 88 81 82 82 89 91 86 offval 
 |-  ( ph -> ( ( X X. { A } ) oF x. F ) = ( x e. X |-> ( A x. ( F ` x ) ) ) )
93 79 87 92 3eqtr4d 
 |-  ( ph -> ( ( S X. { A } ) oF x. F ) = ( ( X X. { A } ) oF x. F ) )
94 93 oveq2d 
 |-  ( ph -> ( S _D ( ( S X. { A } ) oF x. F ) ) = ( S _D ( ( X X. { A } ) oF x. F ) ) )
95 78 mpteq1d 
 |-  ( ph -> ( x e. ( S i^i X ) |-> ( A x. ( ( S _D F ) ` x ) ) ) = ( x e. X |-> ( A x. ( ( S _D F ) ` x ) ) ) )
96 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
97 1 96 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
98 4 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
99 97 98 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
100 99 ffnd 
 |-  ( ph -> ( S _D F ) Fn X )
101 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) = ( ( S _D F ) ` x ) )
102 80 100 1 82 83 85 101 offval 
 |-  ( ph -> ( ( S X. { A } ) oF x. ( S _D F ) ) = ( x e. ( S i^i X ) |-> ( A x. ( ( S _D F ) ` x ) ) ) )
103 0cnd 
 |-  ( ( ph /\ x e. X ) -> 0 e. CC )
104 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. A ) e. _V )
105 72 oveq1d 
 |-  ( ph -> ( ( S _D ( X X. { A } ) ) oF x. F ) = ( ( X X. { 0 } ) oF x. F ) )
106 0cnd 
 |-  ( ph -> 0 e. CC )
107 mul02 
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
108 107 adantl 
 |-  ( ( ph /\ x e. CC ) -> ( 0 x. x ) = 0 )
109 82 2 106 106 108 caofid2 
 |-  ( ph -> ( ( X X. { 0 } ) oF x. F ) = ( X X. { 0 } ) )
110 105 109 eqtrd 
 |-  ( ph -> ( ( S _D ( X X. { A } ) ) oF x. F ) = ( X X. { 0 } ) )
111 110 69 eqtrdi 
 |-  ( ph -> ( ( S _D ( X X. { A } ) ) oF x. F ) = ( x e. X |-> 0 ) )
112 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. _V )
113 3 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
114 99 feqmptd 
 |-  ( ph -> ( S _D F ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )
115 27 a1i 
 |-  ( ph -> ( X X. { A } ) = ( x e. X |-> A ) )
116 82 112 113 114 115 offval2 
 |-  ( ph -> ( ( S _D F ) oF x. ( X X. { A } ) ) = ( x e. X |-> ( ( ( S _D F ) ` x ) x. A ) ) )
117 82 103 104 111 116 offval2 
 |-  ( ph -> ( ( ( S _D ( X X. { A } ) ) oF x. F ) oF + ( ( S _D F ) oF x. ( X X. { A } ) ) ) = ( x e. X |-> ( 0 + ( ( ( S _D F ) ` x ) x. A ) ) ) )
118 99 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. CC )
119 118 113 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. A ) e. CC )
120 119 addid2d 
 |-  ( ( ph /\ x e. X ) -> ( 0 + ( ( ( S _D F ) ` x ) x. A ) ) = ( ( ( S _D F ) ` x ) x. A ) )
121 118 113 mulcomd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. A ) = ( A x. ( ( S _D F ) ` x ) ) )
122 120 121 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( 0 + ( ( ( S _D F ) ` x ) x. A ) ) = ( A x. ( ( S _D F ) ` x ) ) )
123 122 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( 0 + ( ( ( S _D F ) ` x ) x. A ) ) ) = ( x e. X |-> ( A x. ( ( S _D F ) ` x ) ) ) )
124 117 123 eqtrd 
 |-  ( ph -> ( ( ( S _D ( X X. { A } ) ) oF x. F ) oF + ( ( S _D F ) oF x. ( X X. { A } ) ) ) = ( x e. X |-> ( A x. ( ( S _D F ) ` x ) ) ) )
125 95 102 124 3eqtr4d 
 |-  ( ph -> ( ( S X. { A } ) oF x. ( S _D F ) ) = ( ( ( S _D ( X X. { A } ) ) oF x. F ) oF + ( ( S _D F ) oF x. ( X X. { A } ) ) ) )
126 76 94 125 3eqtr4d 
 |-  ( ph -> ( S _D ( ( S X. { A } ) oF x. F ) ) = ( ( S X. { A } ) oF x. ( S _D F ) ) )