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

Metamath Proof Explorer

Theorem dvmptres2

Proof