Metamath Proof Explorer

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 tgioo4 ⊢ ( 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 𝐹 ) ↾ ( 𝐵 (,) 𝐶 ) ) )