Theorem dvres

Description: Restriction of a derivative. Note that our definition of derivative df-dv would still make sense if we demanded that x be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point x when restricted to different subsets containing x ; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ] . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	dvres.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	dvres.t	⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
Assertion	dvres	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvres.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2		dvres.t	⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
3		reldv	⊢ Rel ( 𝑆 D ( 𝐹 ↾ 𝐵 ) )
4		relres	⊢ Rel ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) )
5		simpll	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝑆 ⊆ ℂ )
6		simplr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
7		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
8		fssres	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
9	6 7 8	sylancl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
10		resres	⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) )
11		ffn	⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 )
12		fnresdm	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
13	6 11 12	3syl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
14	13	reseq1d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐵 ) = ( 𝐹 ↾ 𝐵 ) )
15	10 14	syl5eqr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
16	15	feq1d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ↔ ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ) )
17	9 16	mpbid	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
18		simprl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝐴 ⊆ 𝑆 )
19	7 18	sstrid	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑆 )
20	5 17 19	dvcl	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ) → 𝑦 ∈ ℂ )
21	20	ex	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 → 𝑦 ∈ ℂ ) )
22	5 6 18	dvcl	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
23	22	ex	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 → 𝑦 ∈ ℂ ) )
24	23	adantld	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ ) )
25		eqid	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
26	5	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑆 ⊆ ℂ )
27	6	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
28	18	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐴 ⊆ 𝑆 )
29		simplrr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐵 ⊆ 𝑆 )
30		simpr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
31	1 2 25 26 27 28 29 30	dvreslem	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) )
32	31	ex	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑦 ∈ ℂ → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) ) )
33	21 24 32	pm5.21ndd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) )
34		vex	⊢ 𝑦 ∈ V
35	34	brresi	⊢ ( 𝑥 ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) )
36	33 35	bitr4di	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ 𝑥 ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) 𝑦 ) )
37	3 4 36	eqbrrdiv	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )