dvmptntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptntr.s	$⊢ φ \to S \subseteq ℂ$
	dvmptntr.x	$⊢ φ \to X \subseteq S$
	dvmptntr.a	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvmptntr.j	$⊢ J = K ↾_{𝑡} S$
	dvmptntr.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvmptntr.i	$⊢ φ \to int (J) (X) = Y$
Assertion	dvmptntr	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = \frac{d (x \in Y⟼ A)}{d_{S} x}$

Proof

Step	Hyp	Ref	Expression
1		dvmptntr.s	$⊢ φ \to S \subseteq ℂ$
2		dvmptntr.x	$⊢ φ \to X \subseteq S$
3		dvmptntr.a	$⊢ (φ \land x \in X) \to A \in ℂ$
4		dvmptntr.j	$⊢ J = K ↾_{𝑡} S$
5		dvmptntr.k	$⊢ K = TopOpen (ℂ_{fld})$
6		dvmptntr.i	$⊢ φ \to int (J) (X) = Y$
7	5	cnfldtopon	$⊢ K \in TopOn (ℂ)$
8		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
9	7 1 8	sylancr	$⊢ φ \to K ↾_{𝑡} S \in TopOn (S)$
10	4 9	eqeltrid	$⊢ φ \to J \in TopOn (S)$
11		topontop	$⊢ J \in TopOn (S) \to J \in Top$
12	10 11	syl	$⊢ φ \to J \in Top$
13		toponuni	$⊢ J \in TopOn (S) \to S = ⋃ J$
14	10 13	syl	$⊢ φ \to S = ⋃ J$
15	2 14	sseqtrd	$⊢ φ \to X \subseteq ⋃ J$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	ntridm	$⊢ (J \in Top \land X \subseteq ⋃ J) \to int (J) (int (J) (X)) = int (J) (X)$
18	12 15 17	syl2anc	$⊢ φ \to int (J) (int (J) (X)) = int (J) (X)$
19	6	fveq2d	$⊢ φ \to int (J) (int (J) (X)) = int (J) (Y)$
20	18 19	eqtr3d	$⊢ φ \to int (J) (X) = int (J) (Y)$
21	20	reseq2d	$⊢ φ \to {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (X)} = {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (Y)}$
22	3	fmpttd	$⊢ φ \to (x \in X ⟼ A) : X ⟶ ℂ$
23	5 4	dvres	$⊢ ((S \subseteq ℂ \land (x \in X ⟼ A) : X ⟶ ℂ) \land (X \subseteq S \land X \subseteq S)) \to S D ({(x \in X ⟼ A) ↾}_{X}) = {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (X)}$
24	1 22 2 2 23	syl22anc	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{X}) = {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (X)}$
25	16	ntrss2	$⊢ (J \in Top \land X \subseteq ⋃ J) \to int (J) (X) \subseteq X$
26	12 15 25	syl2anc	$⊢ φ \to int (J) (X) \subseteq X$
27	6 26	eqsstrrd	$⊢ φ \to Y \subseteq X$
28	27 2	sstrd	$⊢ φ \to Y \subseteq S$
29	5 4	dvres	$⊢ ((S \subseteq ℂ \land (x \in X ⟼ A) : X ⟶ ℂ) \land (X \subseteq S \land Y \subseteq S)) \to S D ({(x \in X ⟼ A) ↾}_{Y}) = {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (Y)}$
30	1 22 2 28 29	syl22anc	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{Y}) = {\frac{d (x \in X⟼ A)}{d_{S} x} ↾}_{int (J) (Y)}$
31	21 24 30	3eqtr4d	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{X}) = S D ({(x \in X ⟼ A) ↾}_{Y})$
32		ssid	$⊢ X \subseteq X$
33		resmpt	$⊢ X \subseteq X \to {(x \in X ⟼ A) ↾}_{X} = (x \in X ⟼ A)$
34	32 33	mp1i	$⊢ φ \to {(x \in X ⟼ A) ↾}_{X} = (x \in X ⟼ A)$
35	34	oveq2d	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{X}) = \frac{d (x \in X⟼ A)}{d_{S} x}$
36	31 35	eqtr3d	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{Y}) = \frac{d (x \in X⟼ A)}{d_{S} x}$
37	27	resmptd	$⊢ φ \to {(x \in X ⟼ A) ↾}_{Y} = (x \in Y ⟼ A)$
38	37	oveq2d	$⊢ φ \to S D ({(x \in X ⟼ A) ↾}_{Y}) = \frac{d (x \in Y⟼ A)}{d_{S} x}$
39	36 38	eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = \frac{d (x \in Y⟼ A)}{d_{S} x}$

Metamath Proof Explorer

Theorem dvmptntr

Proof