Metamath Proof Explorer

Theorem dvmptres

Description: Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Hypotheses	dvmptadd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
		dvmptadd.a	$⊢ (φ \land x \in X) \to A \in ℂ$
		dvmptadd.b	$⊢ (φ \land x \in X) \to B \in V$
		dvmptadd.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
		dvmptres.y	$⊢ φ \to Y \subseteq X$
		dvmptres.j	$⊢ J = K ↾_{𝑡} S$
		dvmptres.k	$⊢ K = TopOpen (ℂ_{fld})$
		dvmptres.t	$⊢ φ \to Y \in J$
	Assertion	dvmptres	$⊢ φ \to \frac{d (x \in Y⟼ A)}{d_{S} x} = (x \in Y ⟼ B)$

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvmptadd.a	$⊢ (φ \land x \in X) \to A \in ℂ$
3		dvmptadd.b	$⊢ (φ \land x \in X) \to B \in V$
4		dvmptadd.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
5		dvmptres.y	$⊢ φ \to Y \subseteq X$
6		dvmptres.j	$⊢ J = K ↾_{𝑡} S$
7		dvmptres.k	$⊢ K = TopOpen (ℂ_{fld})$
8		dvmptres.t	$⊢ φ \to Y \in J$
9	7	cnfldtop	$⊢ K \in Top$
10		resttop	$⊢ (K \in Top \land S \in \{ℝ, ℂ\}) \to K ↾_{𝑡} S \in Top$
11	9 1 10	sylancr	$⊢ φ \to K ↾_{𝑡} S \in Top$
12	6 11	eqeltrid	$⊢ φ \to J \in Top$
13		isopn3i	$⊢ (J \in Top \land Y \in J) \to int (J) (Y) = Y$
14	12 8 13	syl2anc	$⊢ φ \to int (J) (Y) = Y$
15	1 2 3 4 5 6 7 14	dvmptres2	$⊢ φ \to \frac{d (x \in Y⟼ A)}{d_{S} x} = (x \in Y ⟼ B)$