Theorem dvresioo

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

	Ref	Expression
Assertion	dvresioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	⊢ ℝ ⊆ ℂ
2	1	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ℝ ⊆ ℂ )
3		simpr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
4		simpl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ⊆ ℝ )
5		ioossre	⊢ ( 𝐵 (,) 𝐶 ) ⊆ ℝ
6	5	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐵 (,) 𝐶 ) ⊆ ℝ )
7		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8	7	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
9	7 8	dvres	⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℝ ∧ ( 𝐵 (,) 𝐶 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) 𝐶 ) ) ) )
10	2 3 4 6 9	syl22anc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) 𝐶 ) ) ) )
11		ioontr	⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) 𝐶 ) ) = ( 𝐵 (,) 𝐶 )
12	11	reseq2i	⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) 𝐶 ) )
13	10 12	eqtrdi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) 𝐶 ) ) )