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 ( 𝐹 ↾ 𝐵 ) ) )