dvresioo

Description: Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	dvresioo	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to ℝ D ({F ↾}_{(B, C)}) = {F_{ℝ}^{'} ↾}_{(B, C)}$

Step	Hyp	Ref	Expression
1		ax-resscn	$⊢ ℝ \subseteq ℂ$
2	1	a1i	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to ℝ \subseteq ℂ$
3		simpr	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to F : A ⟶ ℂ$
4		simpl	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to A \subseteq ℝ$
5		ioossre	$⊢ (B, C) \subseteq ℝ$
6	5	a1i	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to (B, C) \subseteq ℝ$
7		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
8		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
9	7 8	dvres	$⊢ ((ℝ \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq ℝ \land (B, C) \subseteq ℝ)) \to ℝ D ({F ↾}_{(B, C)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, C))}$
10	2 3 4 6 9	syl22anc	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to ℝ D ({F ↾}_{(B, C)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, C))}$
11		ioontr	$⊢ int (topGen (ran (.))) ((B, C)) = (B, C)$
12	11	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, C))} = {F_{ℝ}^{'} ↾}_{(B, C)}$
13	10 12	eqtrdi	$⊢ (A \subseteq ℝ \land F : A ⟶ ℂ) \to ℝ D ({F ↾}_{(B, C)}) = {F_{ℝ}^{'} ↾}_{(B, C)}$

Metamath Proof Explorer