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 fvexd ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ V )
14 fvexd ( 𝜑 → ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ∈ V )
15 dvfg ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
16 ffun ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
17 funfvbrb ( Fun ( 𝑆 D 𝐹 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
18 5 15 16 17 4syl ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
19 6 18 mpbid ( 𝜑𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) )
20 dvfg ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
21 ffun ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
22 funfvbrb ( Fun ( 𝑆 D 𝐺 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
23 5 20 21 22 4syl ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
24 7 23 mpbid ( 𝜑𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) )
25 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
26 1 2 3 4 12 13 14 19 24 25 dvaddbr ( 𝜑𝐶 ( 𝑆 D ( 𝐹f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
27 funbrfv ( Fun ( 𝑆 D ( 𝐹f + 𝐺 ) ) → ( 𝐶 ( 𝑆 D ( 𝐹f + 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) → ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) ) )
28 10 26 27 sylc ( 𝜑 → ( ( 𝑆 D ( 𝐹f + 𝐺 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) + ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )