Metamath Proof Explorer

Theorem dvaddf

Description: The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvaddf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvaddf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
dvaddf.df ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
dvaddf.dg ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
Assertion dvaddf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f + ( 𝑆 D 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 dvaddf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvaddf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
4 dvaddf.df ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
5 dvaddf.dg ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
6 dvbsss ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
7 4 6 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
8 1 7 ssexd ⊢ ( 𝜑 → 𝑋 ∈ V )
9 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
10 1 9 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
11 4 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
12 10 11 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
13 12 ffnd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) Fn 𝑋 )
14 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
15 1 14 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
16 5 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
17 15 16 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
18 17 ffnd ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) Fn 𝑋 )
19 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ⟶ ℂ )
20 1 19 syl ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ⟶ ℂ )
21 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
22 1 21 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
23 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
25 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
26 24 2 3 8 8 25 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : 𝑋 ⟶ ℂ )
27 22 26 7 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ⊆ 𝑋 )
28 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ℂ )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ⊆ 𝑆 )
30 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 : 𝑋 ⟶ ℂ )
31 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ⊆ ℂ )
32 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ V )
33 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ∈ V )
34 4 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ∈ 𝑋 ) )
35 34 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐹 ) )
36 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ { ℝ , ℂ } )
37 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
38 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
39 36 9 37 38 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
40 35 39 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
41 5 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ∈ 𝑋 ) )
42 41 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐺 ) )
43 ffun ⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
44 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
45 36 14 43 44 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
46 42 45 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
47 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
48 28 29 30 29 31 32 33 40 46 47 dvaddbr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
49 reldv ⊢ Rel ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) )
50 49 releldmi ⊢ ( 𝑥 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
51 48 50 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
52 27 51 eqelssd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) = 𝑋 )
53 52 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ⟶ ℂ ↔ ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : 𝑋 ⟶ ℂ ) )
54 20 53 mpbid ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : 𝑋 ⟶ ℂ )
55 54 ffnd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) Fn 𝑋 )
56 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
57 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
58 28 29 30 29 36 35 42 dvadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
59 58 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) = ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑥 ) )
60 8 13 18 55 56 57 59 offveq ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f + ( 𝑆 D 𝐺 ) ) = ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
61 60 eqcomd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f + ( 𝑆 D 𝐺 ) ) )