dvres2

Description: Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex-differentiable then it is also real-differentiable. Unlike dvres , there is no simple reverse relation relating real-differentiable functions to complex differentiability, and indeed there are functions like Re ( x ) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015)

		Ref	Expression
	Assertion	dvres2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to {F_{S}^{'} ↾}_{B} \subseteq B D ({F ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({F_{S}^{'} ↾}_{B})$
2	1	a1i	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to Rel ({F_{S}^{'} ↾}_{B})$
3		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
4		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
5		eqid	$⊢ (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
6		simp1l	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to S \subseteq ℂ$
7		simp1r	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to F : A ⟶ ℂ$
8		simp2l	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to A \subseteq S$
9		simp2r	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to B \subseteq S$
10		simp3r	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to x F_{S}^{'} y$
11	6 7 8	dvcl	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \land x F_{S}^{'} y) \to y \in ℂ$
12	10 11	mpdan	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to y \in ℂ$
13		simp3l	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to x \in B$
14	3 4 5 6 7 8 9 12 10 13	dvres2lem	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S) \land (x \in B \land x F_{S}^{'} y)) \to x {({F ↾}_{B})}_{B}^{'} y$
15	14	3expia	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to ((x \in B \land x F_{S}^{'} y) \to x {({F ↾}_{B})}_{B}^{'} y)$
16		vex	$⊢ y \in V$
17	16	brresi	$⊢ x ({F_{S}^{'} ↾}_{B}) y \leftrightarrow (x \in B \land x F_{S}^{'} y)$
18		df-br	$⊢ x ({F_{S}^{'} ↾}_{B}) y \leftrightarrow ⟨x, y⟩ \in ({F_{S}^{'} ↾}_{B})$
19	17 18	bitr3i	$⊢ (x \in B \land x F_{S}^{'} y) \leftrightarrow ⟨x, y⟩ \in ({F_{S}^{'} ↾}_{B})$
20		df-br	$⊢ x {({F ↾}_{B})}_{B}^{'} y \leftrightarrow ⟨x, y⟩ \in {({F ↾}_{B})}_{B}^{'}$
21	15 19 20	3imtr3g	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to (⟨x, y⟩ \in ({F_{S}^{'} ↾}_{B}) \to ⟨x, y⟩ \in {({F ↾}_{B})}_{B}^{'})$
22	2 21	relssdv	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq S \land B \subseteq S)) \to {F_{S}^{'} ↾}_{B} \subseteq B D ({F ↾}_{B})$

Metamath Proof Explorer

Theorem dvres2

Proof