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 ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )