Theorem dvmptres2

Description: Function-builder for derivative: restrict a derivative to a 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 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
	dvmptres2.z	⊢ ( 𝜑 → 𝑍 ⊆ 𝑋 )
	dvmptres2.j	⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
	dvmptres2.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	dvmptres2.i	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑍 ) = 𝑌 )
Assertion	dvmptres2	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvmptadd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3		dvmptadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4		dvmptadd.da	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5		dvmptres2.z	⊢ ( 𝜑 → 𝑍 ⊆ 𝑋 )
6		dvmptres2.j	⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
7		dvmptres2.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
8		dvmptres2.i	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑍 ) = 𝑌 )
9		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
10	1 9	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
11	2	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
12	4	dmeqd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
13	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
14		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
15	13 14	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
16	12 15	eqtrd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
17		dvbsss	⊢ dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⊆ 𝑆
18	16 17	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
19	5 18	sstrd	⊢ ( 𝜑 → 𝑍 ⊆ 𝑆 )
20	7 6	dvres	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ⊆ 𝑆 ∧ 𝑍 ⊆ 𝑆 ) ) → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑍 ) ) = ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) )
21	10 11 18 19 20	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑍 ) ) = ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) )
22	5	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑍 ) = ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) )
23	22	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑍 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) )
24	4	reseq1d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) )
25	8	reseq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) )
26	7	cnfldtopon	⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
27		resttopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
28	26 10 27	sylancr	⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
29	6 28	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑆 ) )
30		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑆 ) → 𝐽 ∈ Top )
31	29 30	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
32		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝐽 )
33	29 32	syl	⊢ ( 𝜑 → 𝑆 = ∪ 𝐽 )
34	19 33	sseqtrd	⊢ ( 𝜑 → 𝑍 ⊆ ∪ 𝐽 )
35		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
36	35	ntrss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑍 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ⊆ 𝑍 )
37	31 34 36	syl2anc	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ⊆ 𝑍 )
38	8 37	eqsstrrd	⊢ ( 𝜑 → 𝑌 ⊆ 𝑍 )
39	38 5	sstrd	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
40	39	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
41	24 25 40	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑍 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
42	21 23 41	3eqtr3d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )