dvsubf

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

	Ref	Expression
Hypotheses	dvsubf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvsubf.f	$⊢ φ \to F : X ⟶ ℂ$
	dvsubf.g	$⊢ φ \to G : X ⟶ ℂ$
	dvsubf.fdv	$⊢ φ \to dom F_{S}^{'} = X$
	dvsubf.gdv	$⊢ φ \to dom G_{S}^{'} = X$
Assertion	dvsubf	$⊢ φ \to S D (F -_{f} G) = F_{S}^{'} -_{f} G_{S}^{'}$

Proof

Step	Hyp	Ref	Expression
1		dvsubf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvsubf.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvsubf.g	$⊢ φ \to G : X ⟶ ℂ$
4		dvsubf.fdv	$⊢ φ \to dom F_{S}^{'} = X$
5		dvsubf.gdv	$⊢ φ \to dom G_{S}^{'} = X$
6	2	ffvelrnda	$⊢ (φ \land x \in X) \to F (x) \in ℂ$
7		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
8	1 7	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
9	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
10	8 9	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
11	10	ffvelrnda	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in ℂ$
12	2	feqmptd	$⊢ φ \to F = (x \in X ⟼ F (x))$
13	12	oveq2d	$⊢ φ \to S D F = \frac{d (x \in X⟼ F (x))}{d_{S} x}$
14	10	feqmptd	$⊢ φ \to S D F = (x \in X ⟼ F_{S}^{'} (x))$
15	13 14	eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ F (x))}{d_{S} x} = (x \in X ⟼ F_{S}^{'} (x))$
16	3	ffvelrnda	$⊢ (φ \land x \in X) \to G (x) \in ℂ$
17		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
18	1 17	syl	$⊢ φ \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
19	5	feq2d	$⊢ φ \to (G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \leftrightarrow G_{S}^{'} : X ⟶ ℂ)$
20	18 19	mpbid	$⊢ φ \to G_{S}^{'} : X ⟶ ℂ$
21	20	ffvelrnda	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) \in ℂ$
22	3	feqmptd	$⊢ φ \to G = (x \in X ⟼ G (x))$
23	22	oveq2d	$⊢ φ \to S D G = \frac{d (x \in X⟼ G (x))}{d_{S} x}$
24	20	feqmptd	$⊢ φ \to S D G = (x \in X ⟼ G_{S}^{'} (x))$
25	23 24	eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ G (x))}{d_{S} x} = (x \in X ⟼ G_{S}^{'} (x))$
26	1 6 11 15 16 21 25	dvmptsub	$⊢ φ \to \frac{d (x \in X⟼ F (x) - G (x))}{d_{S} x} = (x \in X ⟼ F_{S}^{'} (x) - G_{S}^{'} (x))$
27		ovex	$⊢ S D F \in V$
28	27	dmex	$⊢ dom F_{S}^{'} \in V$
29	4 28	eqeltrrdi	$⊢ φ \to X \in V$
30	29 6 16 12 22	offval2	$⊢ φ \to F -_{f} G = (x \in X ⟼ F (x) - G (x))$
31	30	oveq2d	$⊢ φ \to S D (F -_{f} G) = \frac{d (x \in X⟼ F (x) - G (x))}{d_{S} x}$
32	29 11 21 14 24	offval2	$⊢ φ \to F_{S}^{'} -_{f} G_{S}^{'} = (x \in X ⟼ F_{S}^{'} (x) - G_{S}^{'} (x))$
33	26 31 32	3eqtr4d	$⊢ φ \to S D (F -_{f} G) = F_{S}^{'} -_{f} G_{S}^{'}$

Metamath Proof Explorer

Theorem dvsubf

Proof