This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvres2

Description: Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex-differentiable then it is also real-differentiable. Unlike dvres , there is no simple reverse relation relating real-differentiable functions to complex differentiability, and indeed there are functions like Re ( x ) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion dvres2 ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) ⊆ ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( ( 𝑆 D 𝐹 ) ↾ 𝐵 )
2 1 a1i ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → Rel ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) )
3 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
5 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
6 simp1l ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝑆 ⊆ ℂ )
7 simp1r ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
8 simp2l ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝐴 ⊆ 𝑆 )
9 simp2r ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝐵 ⊆ 𝑆 )
10 simp3r ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
11 6 7 8 dvcl ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
12 10 11 mpdan ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝑦 ∈ ℂ )
13 simp3l ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝑥 ∈ 𝐵 )
14 3 4 5 6 7 8 9 12 10 13 dvres2lem ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) → 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 )
15 14 3expia ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ) )
16 vex ⊢ 𝑦 ∈ V
17 16 brresi ⊢ ( 𝑥 ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) )
18 df-br ⊢ ( 𝑥 ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) )
19 17 18 bitr3i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) )
20 df-br ⊢ ( 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) )
21 15 19 20 3imtr3g ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) ) )
22 2 21 relssdv ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) ⊆ ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) )