Metamath Proof Explorer


Theorem dvadd

Description: The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvadd.f ( 𝜑𝐹 : 𝑋 ⟶ ℂ )
dvadd.x ( 𝜑𝑋𝑆 )
dvadd.g ( 𝜑𝐺 : 𝑌 ⟶ ℂ )
dvadd.y ( 𝜑𝑌𝑆 )
dvadd.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
dvadd.df ( 𝜑𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
dvadd.dg ( 𝜑𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
Assertion dvadd ( 𝜑 → ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dvadd.f ( 𝜑𝐹 : 𝑋 ⟶ ℂ )
2 dvadd.x ( 𝜑𝑋𝑆 )
3 dvadd.g ( 𝜑𝐺 : 𝑌 ⟶ ℂ )
4 dvadd.y ( 𝜑𝑌𝑆 )
5 dvadd.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
6 dvadd.df ( 𝜑𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
7 dvadd.dg ( 𝜑𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
8 dvfg ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹f + 𝐺 ) ) ⟶ ℂ )
9 ffun ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) : dom ( 𝑆 D ( 𝐹f + 𝐺 ) ) ⟶ ℂ → Fun ( 𝑆 D ( 𝐹f + 𝐺 ) ) )
10 5 8 9 3syl ( 𝜑 → Fun ( 𝑆 D ( 𝐹f + 𝐺 ) ) )
11 recnprss ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
12 5 11 syl ( 𝜑𝑆 ⊆ ℂ )
13 dvfg ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
14 ffun ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
15 funfvbrb ( Fun ( 𝑆 D 𝐹 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
16 5 13 14 15 4syl ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
17 6 16 mpbid ( 𝜑𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) )
18 dvfg ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
19 ffun ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
20 funfvbrb ( Fun ( 𝑆 D 𝐺 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
21 5 18 19 20 4syl ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
22 7 21 mpbid ( 𝜑𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) )
23 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
24 1 2 3 4 12 17 22 23 dvaddbr ( 𝜑𝐶 ( 𝑆 D ( 𝐹f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
25 funbrfv ( Fun ( 𝑆 D ( 𝐹f + 𝐺 ) ) → ( 𝐶 ( 𝑆 D ( 𝐹f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) → ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) ) )
26 10 24 25 sylc ( 𝜑 → ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )