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 𝐺 ) ) )