Theorem dvmptresicc

Description: Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvmptresicc.f	$$⊢F=\left(x\in ℂ⟼A\right)$$
	dvmptresicc.a	$$⊢\left(\phi \wedge x\in ℂ\right)\to A\in ℂ$$
	dvmptresicc.fdv	$$⊢\phi \to ℂ\mathrm{D}F=\left(x\in ℂ⟼B\right)$$
	dvmptresicc.b	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in ℂ$$
	dvmptresicc.c	$$⊢\phi \to C\in ℝ$$
	dvmptresicc.d	$$⊢\phi \to D\in ℝ$$
Assertion	dvmptresicc	$$⊢\phi \to \frac{d\left(x\in \left[C,D\right]⟼A\right)}{d_{ℝ}x}=\left(x\in \left(C,D\right)⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptresicc.f	$$⊢F=\left(x\in ℂ⟼A\right)$$
2		dvmptresicc.a	$$⊢\left(\phi \wedge x\in ℂ\right)\to A\in ℂ$$
3		dvmptresicc.fdv	$$⊢\phi \to ℂ\mathrm{D}F=\left(x\in ℂ⟼B\right)$$
4		dvmptresicc.b	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in ℂ$$
5		dvmptresicc.c	$$⊢\phi \to C\in ℝ$$
6		dvmptresicc.d	$$⊢\phi \to D\in ℝ$$
7	1	reseq1i	$$⊢{F\upharpoonright }_{\left[C,D\right]}={\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[C,D\right]}$$
8	5 6	iccssred	$$⊢\phi \to \left[C,D\right]\subseteq ℝ$$
9		ax-resscn	$$⊢ℝ\subseteq ℂ$$
10	9	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
11	8 10	sstrd	$$⊢\phi \to \left[C,D\right]\subseteq ℂ$$
12	11	resmptd	$$⊢\phi \to {\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[C,D\right]}=\left(x\in \left[C,D\right]⟼A\right)$$
13	7 12	eqtrid	$$⊢\phi \to {F\upharpoonright }_{\left[C,D\right]}=\left(x\in \left[C,D\right]⟼A\right)$$
14	13	oveq2d	$$⊢\phi \to ℝ\mathrm{D}\left({F\upharpoonright }_{\left[C,D\right]}\right)=\frac{d\left(x\in \left[C,D\right]⟼A\right)}{d_{ℝ}x}$$
15	8	resabs1d	$$⊢\phi \to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[C,D\right]}={F\upharpoonright }_{\left[C,D\right]}$$
16	15	eqcomd	$$⊢\phi \to {F\upharpoonright }_{\left[C,D\right]}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[C,D\right]}$$
17	16	oveq2d	$$⊢\phi \to ℝ\mathrm{D}\left({F\upharpoonright }_{\left[C,D\right]}\right)=ℝ\mathrm{D}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[C,D\right]}\right)$$
18	2 1	fmptd	$$⊢\phi \to F:ℂ⟶ℂ$$
19	18 10	fssresd	$$⊢\phi \to \left({F\upharpoonright }_{ℝ}\right):ℝ⟶ℂ$$
20		ssidd	$$⊢\phi \to ℝ\subseteq ℝ$$
21		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
22	21	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
23	21 22	dvres	$$⊢\left(\left(ℝ\subseteq ℂ\wedge \left({F\upharpoonright }_{ℝ}\right):ℝ⟶ℂ\right)\wedge \left(ℝ\subseteq ℝ\wedge \left[C,D\right]\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[C,D\right]}\right)={{\left({F\upharpoonright }_{ℝ}\right)}_{ℝ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)}$$
24	10 19 20 8 23	syl22anc	$$⊢\phi \to ℝ\mathrm{D}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[C,D\right]}\right)={{\left({F\upharpoonright }_{ℝ}\right)}_{ℝ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)}$$
25		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
26	25	a1i	$$⊢\phi \to ℝ\in \left\{ℝ,ℂ\right\}$$
27		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
28	3	dmeqd	$$⊢\phi \to \mathrm{dom}{F}_{ℂ}^{\prime }=\mathrm{dom}\left(x\in ℂ⟼B\right)$$
29	4	ralrimiva	$$⊢\phi \to \forall x\in ℂB\in ℂ$$
30		dmmptg	$$⊢\forall x\in ℂB\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼B\right)=ℂ$$
31	29 30	syl	$$⊢\phi \to \mathrm{dom}\left(x\in ℂ⟼B\right)=ℂ$$
32	28 31	eqtr2d	$$⊢\phi \to ℂ=\mathrm{dom}{F}_{ℂ}^{\prime }$$
33	10 32	sseqtrd	$$⊢\phi \to ℝ\subseteq \mathrm{dom}{F}_{ℂ}^{\prime }$$
34		dvres3	$$⊢\left(\left(ℝ\in \left\{ℝ,ℂ\right\}\wedge F:ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge ℝ\subseteq \mathrm{dom}{F}_{ℂ}^{\prime }\right)\right)\to ℝ\mathrm{D}\left({F\upharpoonright }_{ℝ}\right)={F_{ℂ}^{\prime }\upharpoonright }_{ℝ}$$
35	26 18 27 33 34	syl22anc	$$⊢\phi \to ℝ\mathrm{D}\left({F\upharpoonright }_{ℝ}\right)={F_{ℂ}^{\prime }\upharpoonright }_{ℝ}$$
36		iccntr	$$⊢\left(C\in ℝ\wedge D\in ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)=\left(C,D\right)$$
37	5 6 36	syl2anc	$$⊢\phi \to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)=\left(C,D\right)$$
38	35 37	reseq12d	$$⊢\phi \to {{\left({F\upharpoonright }_{ℝ}\right)}_{ℝ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)}={\left({F_{ℂ}^{\prime }\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(C,D\right)}$$
39		ioossre	$$⊢\left(C,D\right)\subseteq ℝ$$
40		resabs1	$$⊢\left(C,D\right)\subseteq ℝ\to {\left({F_{ℂ}^{\prime }\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(C,D\right)}={F_{ℂ}^{\prime }\upharpoonright }_{\left(C,D\right)}$$
41	39 40	mp1i	$$⊢\phi \to {\left({F_{ℂ}^{\prime }\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(C,D\right)}={F_{ℂ}^{\prime }\upharpoonright }_{\left(C,D\right)}$$
42	3	reseq1d	$$⊢\phi \to {F_{ℂ}^{\prime }\upharpoonright }_{\left(C,D\right)}={\left(x\in ℂ⟼B\right)\upharpoonright }_{\left(C,D\right)}$$
43		ioosscn	$$⊢\left(C,D\right)\subseteq ℂ$$
44		resmpt	$$⊢\left(C,D\right)\subseteq ℂ\to {\left(x\in ℂ⟼B\right)\upharpoonright }_{\left(C,D\right)}=\left(x\in \left(C,D\right)⟼B\right)$$
45	43 44	mp1i	$$⊢\phi \to {\left(x\in ℂ⟼B\right)\upharpoonright }_{\left(C,D\right)}=\left(x\in \left(C,D\right)⟼B\right)$$
46	42 45	eqtrd	$$⊢\phi \to {F_{ℂ}^{\prime }\upharpoonright }_{\left(C,D\right)}=\left(x\in \left(C,D\right)⟼B\right)$$
47	38 41 46	3eqtrd	$$⊢\phi \to {{\left({F\upharpoonright }_{ℝ}\right)}_{ℝ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[C,D\right]\right)}=\left(x\in \left(C,D\right)⟼B\right)$$
48	17 24 47	3eqtrd	$$⊢\phi \to ℝ\mathrm{D}\left({F\upharpoonright }_{\left[C,D\right]}\right)=\left(x\in \left(C,D\right)⟼B\right)$$
49	14 48	eqtr3d	$$⊢\phi \to \frac{d\left(x\in \left[C,D\right]⟼A\right)}{d_{ℝ}x}=\left(x\in \left(C,D\right)⟼B\right)$$