dvaddf

Description: The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dvaddf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvaddf.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvaddf.g	$⊢ φ \to G : X ⟶ ℂ$
4		dvaddf.df	$⊢ φ \to dom F_{S}^{'} = X$
5		dvaddf.dg	$⊢ φ \to dom G_{S}^{'} = X$
6		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
7	4 6	eqsstrrdi	$⊢ φ \to X \subseteq S$
8	1 7	ssexd	$⊢ φ \to X \in V$
9		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
10	1 9	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
11	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
12	10 11	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
13	12	ffnd	$⊢ φ \to F_{S}^{'} Fn X$
14		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
15	1 14	syl	$⊢ φ \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
16	5	feq2d	$⊢ φ \to (G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \leftrightarrow G_{S}^{'} : X ⟶ ℂ)$
17	15 16	mpbid	$⊢ φ \to G_{S}^{'} : X ⟶ ℂ$
18	17	ffnd	$⊢ φ \to G_{S}^{'} Fn X$
19		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {(F +_{f} G)}_{S}^{'} : dom {(F +_{f} G)}_{S}^{'} ⟶ ℂ$
20	1 19	syl	$⊢ φ \to {(F +_{f} G)}_{S}^{'} : dom {(F +_{f} G)}_{S}^{'} ⟶ ℂ$
21		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
22	1 21	syl	$⊢ φ \to S \subseteq ℂ$
23		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
24	23	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
25		inidm	$⊢ X \cap X = X$
26	24 2 3 8 8 25	off	$⊢ φ \to (F +_{f} G) : X ⟶ ℂ$
27	22 26 7	dvbss	$⊢ φ \to dom {(F +_{f} G)}_{S}^{'} \subseteq X$
28	2	adantr	$⊢ (φ \land x \in X) \to F : X ⟶ ℂ$
29	7	adantr	$⊢ (φ \land x \in X) \to X \subseteq S$
30	3	adantr	$⊢ (φ \land x \in X) \to G : X ⟶ ℂ$
31	22	adantr	$⊢ (φ \land x \in X) \to S \subseteq ℂ$
32		fvexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in V$
33		fvexd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) \in V$
34	4	eleq2d	$⊢ φ \to (x \in dom F_{S}^{'} \leftrightarrow x \in X)$
35	34	biimpar	$⊢ (φ \land x \in X) \to x \in dom F_{S}^{'}$
36	1	adantr	$⊢ (φ \land x \in X) \to S \in \{ℝ, ℂ\}$
37		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
38		funfvbrb	$⊢ Fun F_{S}^{'} \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
39	36 9 37 38	4syl	$⊢ (φ \land x \in X) \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
40	35 39	mpbid	$⊢ (φ \land x \in X) \to x F_{S}^{'} F_{S}^{'} (x)$
41	5	eleq2d	$⊢ φ \to (x \in dom G_{S}^{'} \leftrightarrow x \in X)$
42	41	biimpar	$⊢ (φ \land x \in X) \to x \in dom G_{S}^{'}$
43		ffun	$⊢ G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \to Fun G_{S}^{'}$
44		funfvbrb	$⊢ Fun G_{S}^{'} \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
45	36 14 43 44	4syl	$⊢ (φ \land x \in X) \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
46	42 45	mpbid	$⊢ (φ \land x \in X) \to x G_{S}^{'} G_{S}^{'} (x)$
47		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
48	28 29 30 29 31 32 33 40 46 47	dvaddbr	$⊢ (φ \land x \in X) \to x {(F +_{f} G)}_{S}^{'} (F_{S}^{'} (x) + G_{S}^{'} (x))$
49		reldv	$⊢ Rel {(F +_{f} G)}_{S}^{'}$
50	49	releldmi	$⊢ x {(F +_{f} G)}_{S}^{'} (F_{S}^{'} (x) + G_{S}^{'} (x)) \to x \in dom {(F +_{f} G)}_{S}^{'}$
51	48 50	syl	$⊢ (φ \land x \in X) \to x \in dom {(F +_{f} G)}_{S}^{'}$
52	27 51	eqelssd	$⊢ φ \to dom {(F +_{f} G)}_{S}^{'} = X$
53	52	feq2d	$⊢ φ \to ({(F +_{f} G)}_{S}^{'} : dom {(F +_{f} G)}_{S}^{'} ⟶ ℂ \leftrightarrow {(F +_{f} G)}_{S}^{'} : X ⟶ ℂ)$
54	20 53	mpbid	$⊢ φ \to {(F +_{f} G)}_{S}^{'} : X ⟶ ℂ$
55	54	ffnd	$⊢ φ \to {(F +_{f} G)}_{S}^{'} Fn X$
56		eqidd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) = F_{S}^{'} (x)$
57		eqidd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) = G_{S}^{'} (x)$
58	28 29 30 29 36 35 42	dvadd	$⊢ (φ \land x \in X) \to {(F +_{f} G)}_{S}^{'} (x) = F_{S}^{'} (x) + G_{S}^{'} (x)$
59	58	eqcomd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) + G_{S}^{'} (x) = {(F +_{f} G)}_{S}^{'} (x)$
60	8 13 18 55 56 57 59	offveq	$⊢ φ \to F_{S}^{'} +_{f} G_{S}^{'} = S D (F +_{f} G)$
61	60	eqcomd	$⊢ φ \to S D (F +_{f} G) = F_{S}^{'} +_{f} G_{S}^{'}$

Metamath Proof Explorer

Theorem dvaddf

Proof