Metamath Proof Explorer


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 eqtr3id ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴𝑆𝐵𝑆 ) ) → ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐹𝐵 ) )
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 ‘ 𝑇 ) ‘ 𝐵 ) ) )