This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvmptres

Description: Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptres.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
dvmptres.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
dvmptres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvmptres.t ⊢ ( 𝜑 → 𝑌 ∈ 𝐽 )
Assertion dvmptres ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 dvmptres.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
6 dvmptres.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
7 dvmptres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
8 dvmptres.t ⊢ ( 𝜑 → 𝑌 ∈ 𝐽 )
9 7 cnfldtop ⊢ 𝐾 ∈ Top
10 resttop ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
11 9 1 10 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ Top )
12 6 11 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ Top )
13 isopn3i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑌 ) = 𝑌 )
14 12 8 13 syl2anc ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑌 ) = 𝑌 )
15 1 2 3 4 5 6 7 14 dvmptres2 ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )