# Metamath Proof Explorer

## Theorem dvmptres2

Description: Function-builder for derivative: restrict a derivative to a subset. (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)$
dvmptres2.z ${⊢}{\phi }\to {Z}\subseteq {X}$
dvmptres2.j ${⊢}{J}={K}{↾}_{𝑡}{S}$
dvmptres2.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
dvmptres2.i ${⊢}{\phi }\to \mathrm{int}\left({J}\right)\left({Z}\right)={Y}$
Assertion dvmptres2 ${⊢}{\phi }\to \frac{d\left({x}\in {Z}⟼{A}\right)}{{d}_{{S}}{x}}=\left({x}\in {Y}⟼{B}\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 dvmptres2.z ${⊢}{\phi }\to {Z}\subseteq {X}$
6 dvmptres2.j ${⊢}{J}={K}{↾}_{𝑡}{S}$
7 dvmptres2.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
8 dvmptres2.i ${⊢}{\phi }\to \mathrm{int}\left({J}\right)\left({Z}\right)={Y}$
9 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
10 1 9 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
11 2 fmpttd ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}⟶ℂ$
12 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)$
13 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in {V}$
14 dmmptg ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in {V}\to \mathrm{dom}\left({x}\in {X}⟼{B}\right)={X}$
15 13 14 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {X}⟼{B}\right)={X}$
16 12 15 eqtrd ${⊢}{\phi }\to \mathrm{dom}\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}={X}$
17 dvbsss ${⊢}\mathrm{dom}\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}\subseteq {S}$
18 16 17 eqsstrrdi ${⊢}{\phi }\to {X}\subseteq {S}$
19 5 18 sstrd ${⊢}{\phi }\to {Z}\subseteq {S}$
20 7 6 dvres ${⊢}\left(\left({S}\subseteq ℂ\wedge \left({x}\in {X}⟼{A}\right):{X}⟶ℂ\right)\wedge \left({X}\subseteq {S}\wedge {Z}\subseteq {S}\right)\right)\to {S}\mathrm{D}\left({\left({x}\in {X}⟼{A}\right)↾}_{{Z}}\right)={\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}$
21 10 11 18 19 20 syl22anc ${⊢}{\phi }\to {S}\mathrm{D}\left({\left({x}\in {X}⟼{A}\right)↾}_{{Z}}\right)={\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}$
22 5 resmptd ${⊢}{\phi }\to {\left({x}\in {X}⟼{A}\right)↾}_{{Z}}=\left({x}\in {Z}⟼{A}\right)$
23 22 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left({\left({x}\in {X}⟼{A}\right)↾}_{{Z}}\right)=\frac{d\left({x}\in {Z}⟼{A}\right)}{{d}_{{S}}{x}}$
24 4 reseq1d ${⊢}{\phi }\to {\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}={\left({x}\in {X}⟼{B}\right)↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}$
25 8 reseq2d ${⊢}{\phi }\to {\left({x}\in {X}⟼{B}\right)↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}={\left({x}\in {X}⟼{B}\right)↾}_{{Y}}$
26 7 cnfldtopon ${⊢}{K}\in \mathrm{TopOn}\left(ℂ\right)$
27 resttopon ${⊢}\left({K}\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to {K}{↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
28 26 10 27 sylancr ${⊢}{\phi }\to {K}{↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
29 6 28 eqeltrid ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({S}\right)$
30 topontop ${⊢}{J}\in \mathrm{TopOn}\left({S}\right)\to {J}\in \mathrm{Top}$
31 29 30 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
32 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({S}\right)\to {S}=\bigcup {J}$
33 29 32 syl ${⊢}{\phi }\to {S}=\bigcup {J}$
34 19 33 sseqtrd ${⊢}{\phi }\to {Z}\subseteq \bigcup {J}$
35 eqid ${⊢}\bigcup {J}=\bigcup {J}$
36 35 ntrss2 ${⊢}\left({J}\in \mathrm{Top}\wedge {Z}\subseteq \bigcup {J}\right)\to \mathrm{int}\left({J}\right)\left({Z}\right)\subseteq {Z}$
37 31 34 36 syl2anc ${⊢}{\phi }\to \mathrm{int}\left({J}\right)\left({Z}\right)\subseteq {Z}$
38 8 37 eqsstrrd ${⊢}{\phi }\to {Y}\subseteq {Z}$
39 38 5 sstrd ${⊢}{\phi }\to {Y}\subseteq {X}$
40 39 resmptd ${⊢}{\phi }\to {\left({x}\in {X}⟼{B}\right)↾}_{{Y}}=\left({x}\in {Y}⟼{B}\right)$
41 24 25 40 3eqtrd ${⊢}{\phi }\to {\frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}↾}_{\mathrm{int}\left({J}\right)\left({Z}\right)}=\left({x}\in {Y}⟼{B}\right)$
42 21 23 41 3eqtr3d ${⊢}{\phi }\to \frac{d\left({x}\in {Z}⟼{A}\right)}{{d}_{{S}}{x}}=\left({x}\in {Y}⟼{B}\right)$