Theorem dvmptres3

Description: Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptres3.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	dvmptres3.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvmptres3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
	dvmptres3.y	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑌 )
	dvmptres3.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvmptres3.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
	dvmptres3.d	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion	dvmptres3	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptres3.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		dvmptres3.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3		dvmptres3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
4		dvmptres3.y	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑌 )
5		dvmptres3.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
6		dvmptres3.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
7		dvmptres3.d	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
8	5	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
9	7	dmeqd	⊢ ( 𝜑 → dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
10		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
11	10 6	dmmptd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
12	9 11	eqtrd	⊢ ( 𝜑 → dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
13	1	dvres3a	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ∈ 𝐽 ∧ dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 ) ) → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
14	2 8 3 12 13	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
15		rescom	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ↾ 𝑋 )
16		resres	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) )
17	15 16	eqtri	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) )
18	4	reseq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) )
19	17 18	syl5eq	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) )
20		ffn	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) Fn 𝑋 )
21		fnresdm	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) Fn 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
22	8 20 21	3syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
23	22	reseq1d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) )
24		inss2	⊢ ( 𝑆 ∩ 𝑋 ) ⊆ 𝑋
25	4 24	eqsstrrdi	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
26	25	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) )
27	19 23 26	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) )
28	27	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) )
29		rescom	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑆 ) ↾ 𝑋 )
30		resres	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑆 ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) )
31	29 30	eqtri	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) )
32	4	reseq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) )
33	31 32	syl5eq	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) )
34	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
35	10	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) Fn 𝑋 )
36		fnresdm	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) Fn 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
37	34 35 36	3syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
38	37 7	eqtr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
39	38	reseq1d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
40	25	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
41	33 39 40	3eqtr3d	⊢ ( 𝜑 → ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
42	14 28 41	3eqtr3d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )