Metamath Proof Explorer

Theorem dvres3

Description: Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvres3 ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 reldv ⊢ Rel ( 𝑆 D ( 𝐹 ↾ 𝑆 ) )
2 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
3 2 ad2antrr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝑆 ⊆ ℂ )
4 simplr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝐹 : 𝐴 ⟶ ℂ )
5 simprr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝑆 ⊆ dom ( ℂ D 𝐹 ) )
6 ssidd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ℂ ⊆ ℂ )
7 simprl ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝐴 ⊆ ℂ )
8 6 4 7 dvbss ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → dom ( ℂ D 𝐹 ) ⊆ 𝐴 )
9 5 8 sstrd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝑆 ⊆ 𝐴 )
10 4 9 fssresd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( 𝐹 ↾ 𝑆 ) : 𝑆 ⟶ ℂ )
11 ssidd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → 𝑆 ⊆ 𝑆 )
12 3 10 11 dvbss ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ 𝑆 )
13 ssdmres ⊢ ( 𝑆 ⊆ dom ( ℂ D 𝐹 ) ↔ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) = 𝑆 )
14 5 13 sylib ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) = 𝑆 )
15 12 14 sseqtrrd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )
16 relssres ⊢ ( ( Rel ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ∧ dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⊆ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) )
17 1 15 16 sylancr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) )
18 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) : dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⟶ ℂ )
19 18 ad2antrr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) : dom ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ⟶ ℂ )
20 19 ffund ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → Fun ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) )
21 dvres2 ⊢ ( ( ( ℂ ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ ℂ ) ) → ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) )
22 6 4 7 3 21 syl22anc ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) )
23 funssres ⊢ ( ( Fun ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ∧ ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ⊆ ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )
24 20 22 23 syl2anc ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) ↾ dom ( ( ℂ D 𝐹 ) ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )
25 17 24 eqtr3d ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D 𝐹 ) ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑆 ) ) = ( ( ℂ D 𝐹 ) ↾ 𝑆 ) )