dvres

Description: Restriction of a derivative. Note that our definition of derivative df-dv would still make sense if we demanded that x be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point x when restricted to different subsets containing x ; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ] . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvres.t	$⊢ T = K ↾_{𝑡} S$
Assertion	dvres	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to S D ({F ↾}_{B}) = {F_{S}^{'} ↾}_{int (T) (B)}$

Proof

Step	Hyp	Ref	Expression
1		dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
2		dvres.t	$⊢ T = K ↾_{𝑡} S$
3		reldv	$⊢ Rel {({F ↾}_{B})}_{S}^{'}$
4		relres	$⊢ Rel ({F_{S}^{'} ↾}_{int (T) (B)})$
5		simpll	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to S \subseteq ℂ$
6		simplr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to F : A ⟶ ℂ$
7		inss1	$⊢ A \cap B \subseteq A$
8		fssres	$⊢ (F : A ⟶ ℂ \land A \cap B \subseteq A) \to ({F ↾}_{(A \cap B)}) : A \cap B ⟶ ℂ$
9	6 7 8	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to ({F ↾}_{(A \cap B)}) : A \cap B ⟶ ℂ$
10		resres	$⊢ {({F ↾}_{A}) ↾}_{B} = {F ↾}_{(A \cap B)}$
11		ffn	$⊢ F : A ⟶ ℂ \to F Fn A$
12		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
13	6 11 12	3syl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to {F ↾}_{A} = F$
14	13	reseq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to {({F ↾}_{A}) ↾}_{B} = {F ↾}_{B}$
15	10 14	eqtr3id	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to {F ↾}_{(A \cap B)} = {F ↾}_{B}$
16	15	feq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (({F ↾}_{(A \cap B)}) : A \cap B ⟶ ℂ \leftrightarrow ({F ↾}_{B}) : A \cap B ⟶ ℂ)$
17	9 16	mpbid	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to ({F ↾}_{B}) : A \cap B ⟶ ℂ$
18		simprl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to A \subseteq S$
19	7 18	sstrid	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to A \cap B \subseteq S$
20	5 17 19	dvcl	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land x {({F ↾}_{B})}_{S}^{'} y) \to y \in ℂ$
21	20	ex	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (x {({F ↾}_{B})}_{S}^{'} y \to y \in ℂ)$
22	5 6 18	dvcl	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land x F_{S}^{'} y) \to y \in ℂ$
23	22	ex	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (x F_{S}^{'} y \to y \in ℂ)$
24	23	adantld	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to ((x \in int (T) (B) \land x F_{S}^{'} y) \to y \in ℂ)$
25		eqid	$⊢ (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
26	5	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to S \subseteq ℂ$
27	6	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to F : A ⟶ ℂ$
28	18	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to A \subseteq S$
29		simplrr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to B \subseteq S$
30		simpr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to y \in ℂ$
31	1 2 25 26 27 28 29 30	dvreslem	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \land y \in ℂ) \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y))$
32	31	ex	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (y \in ℂ \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y)))$
33	21 24 32	pm5.21ndd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y))$
34		vex	$⊢ y \in V$
35	34	brresi	$⊢ x ({F_{S}^{'} ↾}_{int (T) (B)}) y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y)$
36	33 35	bitr4di	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow x ({F_{S}^{'} ↾}_{int (T) (B)}) y)$
37	3 4 36	eqbrrdiv	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to S D ({F ↾}_{B}) = {F_{S}^{'} ↾}_{int (T) (B)}$

Metamath Proof Explorer

Theorem dvres

Proof