Theorem dvmptcmul

Description: Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
	dvmptcmul.c	$$⊢\phi \to C\in ℂ$$
Assertion	dvmptcmul	$$⊢\phi \to \frac{d\left(x\in X⟼CA\right)}{d_{S}x}=\left(x\in X⟼CB\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
3		dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
4		dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
5		dvmptcmul.c	$$⊢\phi \to C\in ℂ$$
6	5	adantr	$$⊢\left(\phi \wedge x\in X\right)\to C\in ℂ$$
7		0cnd	$$⊢\left(\phi \wedge x\in X\right)\to 0\in ℂ$$
8	5	adantr	$$⊢\left(\phi \wedge x\in S\right)\to C\in ℂ$$
9		0cnd	$$⊢\left(\phi \wedge x\in S\right)\to 0\in ℂ$$
10	1 5	dvmptc	$$⊢\phi \to \frac{d\left(x\in S⟼C\right)}{d_{S}x}=\left(x\in S⟼0\right)$$
11	4	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}=\mathrm{dom}\left(x\in X⟼B\right)$$
12	3	ralrimiva	$$⊢\phi \to \forall x\in XB\in V$$
13		dmmptg	$$⊢\forall x\in XB\in V\to \mathrm{dom}\left(x\in X⟼B\right)=X$$
14	12 13	syl	$$⊢\phi \to \mathrm{dom}\left(x\in X⟼B\right)=X$$
15	11 14	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}=X$$
16		dvbsss	$$⊢\mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}\subseteq S$$
17	15 16	eqsstrrdi	$$⊢\phi \to X\subseteq S$$
18		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S$$
19		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
20	19	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
21		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
22	1 21	syl	$$⊢\phi \to S\subseteq ℂ$$
23		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge S\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
24	20 22 23	sylancr	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
25		topontop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
26	24 25	syl	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
27		toponuni	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)\to S=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
28	24 27	syl	$$⊢\phi \to S=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
29	17 28	sseqtrd	$$⊢\phi \to X\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
30		eqid	$$⊢\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
31	30	ntrss2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Top}\wedge X\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(X\right)\subseteq X$$
32	26 29 31	syl2anc	$$⊢\phi \to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(X\right)\subseteq X$$
33	2	fmpttd	$$⊢\phi \to \left(x\in X⟼A\right):X⟶ℂ$$
34	22 33 17 18 19	dvbssntr	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(X\right)$$
35	15 34	eqsstrrd	$$⊢\phi \to X\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(X\right)$$
36	32 35	eqssd	$$⊢\phi \to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(X\right)=X$$
37	1 8 9 10 17 18 19 36	dvmptres2	$$⊢\phi \to \frac{d\left(x\in X⟼C\right)}{d_{S}x}=\left(x\in X⟼0\right)$$
38	1 6 7 37 2 3 4	dvmptmul	$$⊢\phi \to \frac{d\left(x\in X⟼CA\right)}{d_{S}x}=\left(x\in X⟼0\cdot A+BC\right)$$
39	2	mul02d	$$⊢\left(\phi \wedge x\in X\right)\to 0\cdot A=0$$
40	39	oveq1d	$$⊢\left(\phi \wedge x\in X\right)\to 0\cdot A+BC=0+BC$$
41	1 2 3 4	dvmptcl	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$
42	41 6	mulcld	$$⊢\left(\phi \wedge x\in X\right)\to BC\in ℂ$$
43	42	addlidd	$$⊢\left(\phi \wedge x\in X\right)\to 0+BC=BC$$
44	41 6	mulcomd	$$⊢\left(\phi \wedge x\in X\right)\to BC=CB$$
45	40 43 44	3eqtrd	$$⊢\left(\phi \wedge x\in X\right)\to 0\cdot A+BC=CB$$
46	45	mpteq2dva	$$⊢\phi \to \left(x\in X⟼0\cdot A+BC\right)=\left(x\in X⟼CB\right)$$
47	38 46	eqtrd	$$⊢\phi \to \frac{d\left(x\in X⟼CA\right)}{d_{S}x}=\left(x\in X⟼CB\right)$$