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 4 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ∈ 𝑋 ) )
33 32 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐹 ) )
34 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ { ℝ , ℂ } )
35 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
36 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
37 34 9 35 36 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
38 33 37 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
39 5 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ∈ 𝑋 ) )
40 39 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐺 ) )
41 ffun ⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
42 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
43 34 14 41 42 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
44 40 43 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
45 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
46 28 29 30 29 31 38 44 45 dvaddbr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
47 reldv ⊢ Rel ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) )
48 47 releldmi ⊢ ( 𝑥 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
49 46 48 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
50 27 49 eqelssd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) = 𝑋 )
51 50 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ⟶ ℂ ↔ ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : 𝑋 ⟶ ℂ ) )
52 20 51 mpbid ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) : 𝑋 ⟶ ℂ )
53 52 ffnd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) Fn 𝑋 )
54 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
55 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
56 28 29 30 29 34 33 40 dvadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
57 56 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) = ( ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑥 ) )
58 8 13 18 53 54 55 57 offveq ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f + ( 𝑆 D 𝐺 ) ) = ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) )
59 58 eqcomd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f + ( 𝑆 D 𝐺 ) ) )