This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvsubf

Description: The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvsubf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvsubf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvsubf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
dvsubf.fdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
dvsubf.gdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
Assertion dvsubf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f − ( 𝑆 D 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 dvsubf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvsubf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvsubf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
4 dvsubf.fdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
5 dvsubf.gdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
6 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
7 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
8 1 7 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
9 4 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
10 8 9 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
12 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
13 12 oveq2d ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
14 10 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
15 13 14 eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
16 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
17 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
18 1 17 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
19 5 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
20 18 19 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
21 20 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ∈ ℂ )
22 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
23 22 oveq2d ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
24 20 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
25 23 24 eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
26 1 6 11 15 16 21 25 dvmptsub ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) − ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) ) )
27 ovex ⊢ ( 𝑆 D 𝐹 ) ∈ V
28 27 dmex ⊢ dom ( 𝑆 D 𝐹 ) ∈ V
29 4 28 eqeltrrdi ⊢ ( 𝜑 → 𝑋 ∈ V )
30 29 6 16 12 22 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) )
32 29 11 21 14 24 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f − ( 𝑆 D 𝐺 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) − ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) ) )
33 26 31 32 3eqtr4d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f − ( 𝑆 D 𝐺 ) ) )