Metamath Proof Explorer

Theorem dvmptresicc

Description: Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptresicc.f ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐴 )
dvmptresicc.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
dvmptresicc.fdv ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
dvmptresicc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
dvmptresicc.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
dvmptresicc.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
Assertion dvmptresicc ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvmptresicc.f ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐴 )
2 dvmptresicc.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
3 dvmptresicc.fdv ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
4 dvmptresicc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 dvmptresicc.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 dvmptresicc.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7 1 reseq1i ⊢ ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) = ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 𝐶 [,] 𝐷 ) )
8 5 6 iccssred ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 9 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
11 8 10 sstrd ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℂ )
12 11 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 𝐶 [,] 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ 𝐴 ) )
13 7 12 eqtrid ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ 𝐴 ) )
14 13 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ 𝐴 ) ) )
15 8 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ( 𝐶 [,] 𝐷 ) ) = ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) )
16 15 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) = ( ( 𝐹 ↾ ℝ ) ↾ ( 𝐶 [,] 𝐷 ) ) )
17 16 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ) = ( ℝ D ( ( 𝐹 ↾ ℝ ) ↾ ( 𝐶 [,] 𝐷 ) ) ) )
18 2 1 fmptd ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
19 18 10 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℂ )
20 ssidd ⊢ ( 𝜑 → ℝ ⊆ ℝ )
21 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
22 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
23 21 22 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐶 [,] 𝐷 ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝐹 ↾ ℝ ) ↾ ( 𝐶 [,] 𝐷 ) ) ) = ( ( ℝ D ( 𝐹 ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) ) )
24 10 19 20 8 23 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝐹 ↾ ℝ ) ↾ ( 𝐶 [,] 𝐷 ) ) ) = ( ( ℝ D ( 𝐹 ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) ) )
25 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
26 25 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
27 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
28 3 dmeqd ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) = dom ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
29 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ 𝐵 ∈ ℂ )
30 dmmptg ⊢ ( ∀ 𝑥 ∈ ℂ 𝐵 ∈ ℂ → dom ( 𝑥 ∈ ℂ ↦ 𝐵 ) = ℂ )
31 29 30 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ ℂ ↦ 𝐵 ) = ℂ )
32 28 31 eqtr2d ⊢ ( 𝜑 → ℂ = dom ( ℂ D 𝐹 ) )
33 10 32 sseqtrd ⊢ ( 𝜑 → ℝ ⊆ dom ( ℂ D 𝐹 ) )
34 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) ) → ( ℝ D ( 𝐹 ↾ ℝ ) ) = ( ( ℂ D 𝐹 ) ↾ ℝ ) )
35 26 18 27 33 34 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ℝ ) ) = ( ( ℂ D 𝐹 ) ↾ ℝ ) )
36 iccntr ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) = ( 𝐶 (,) 𝐷 ) )
37 5 6 36 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) = ( 𝐶 (,) 𝐷 ) )
38 35 37 reseq12d ⊢ ( 𝜑 → ( ( ℝ D ( 𝐹 ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) ) = ( ( ( ℂ D 𝐹 ) ↾ ℝ ) ↾ ( 𝐶 (,) 𝐷 ) ) )
39 ioossre ⊢ ( 𝐶 (,) 𝐷 ) ⊆ ℝ
40 resabs1 ⊢ ( ( 𝐶 (,) 𝐷 ) ⊆ ℝ → ( ( ( ℂ D 𝐹 ) ↾ ℝ ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( ( ℂ D 𝐹 ) ↾ ( 𝐶 (,) 𝐷 ) ) )
41 39 40 mp1i ⊢ ( 𝜑 → ( ( ( ℂ D 𝐹 ) ↾ ℝ ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( ( ℂ D 𝐹 ) ↾ ( 𝐶 (,) 𝐷 ) ) )
42 3 reseq1d ⊢ ( 𝜑 → ( ( ℂ D 𝐹 ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( ( 𝑥 ∈ ℂ ↦ 𝐵 ) ↾ ( 𝐶 (,) 𝐷 ) ) )
43 ioosscn ⊢ ( 𝐶 (,) 𝐷 ) ⊆ ℂ
44 resmpt ⊢ ( ( 𝐶 (,) 𝐷 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ 𝐵 ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )
45 43 44 mp1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ 𝐵 ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )
46 42 45 eqtrd ⊢ ( 𝜑 → ( ( ℂ D 𝐹 ) ↾ ( 𝐶 (,) 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )
47 38 41 46 3eqtrd ⊢ ( 𝜑 → ( ( ℝ D ( 𝐹 ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 [,] 𝐷 ) ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )
48 17 24 47 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )
49 14 48 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ↦ 𝐵 ) )