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	4	eleq2d	$⊢ φ \to (x \in dom F_{S}^{'} \leftrightarrow x \in X)$
33	32	biimpar	$⊢ (φ \land x \in X) \to x \in dom F_{S}^{'}$
34	1	adantr	$⊢ (φ \land x \in X) \to S \in \{ℝ, ℂ\}$
35		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
36		funfvbrb	$⊢ Fun F_{S}^{'} \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
37	34 9 35 36	4syl	$⊢ (φ \land x \in X) \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
38	33 37	mpbid	$⊢ (φ \land x \in X) \to x F_{S}^{'} F_{S}^{'} (x)$
39	5	eleq2d	$⊢ φ \to (x \in dom G_{S}^{'} \leftrightarrow x \in X)$
40	39	biimpar	$⊢ (φ \land x \in X) \to x \in dom G_{S}^{'}$
41		ffun	$⊢ G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \to Fun G_{S}^{'}$
42		funfvbrb	$⊢ Fun G_{S}^{'} \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
43	34 14 41 42	4syl	$⊢ (φ \land x \in X) \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
44	40 43	mpbid	$⊢ (φ \land x \in X) \to x G_{S}^{'} G_{S}^{'} (x)$
45		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
46	28 29 30 29 31 38 44 45	dvaddbr	$⊢ (φ \land x \in X) \to x {(F +_{f} G)}_{S}^{'} (F_{S}^{'} (x) + G_{S}^{'} (x))$
47		reldv	$⊢ Rel {(F +_{f} G)}_{S}^{'}$
48	47	releldmi	$⊢ x {(F +_{f} G)}_{S}^{'} (F_{S}^{'} (x) + G_{S}^{'} (x)) \to x \in dom {(F +_{f} G)}_{S}^{'}$
49	46 48	syl	$⊢ (φ \land x \in X) \to x \in dom {(F +_{f} G)}_{S}^{'}$
50	27 49	eqelssd	$⊢ φ \to dom {(F +_{f} G)}_{S}^{'} = X$
51	50	feq2d	$⊢ φ \to ({(F +_{f} G)}_{S}^{'} : dom {(F +_{f} G)}_{S}^{'} ⟶ ℂ \leftrightarrow {(F +_{f} G)}_{S}^{'} : X ⟶ ℂ)$
52	20 51	mpbid	$⊢ φ \to {(F +_{f} G)}_{S}^{'} : X ⟶ ℂ$
53	52	ffnd	$⊢ φ \to {(F +_{f} G)}_{S}^{'} Fn X$
54		eqidd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) = F_{S}^{'} (x)$
55		eqidd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) = G_{S}^{'} (x)$
56	28 29 30 29 34 33 40	dvadd	$⊢ (φ \land x \in X) \to {(F +_{f} G)}_{S}^{'} (x) = F_{S}^{'} (x) + G_{S}^{'} (x)$
57	56	eqcomd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) + G_{S}^{'} (x) = {(F +_{f} G)}_{S}^{'} (x)$
58	8 13 18 53 54 55 57	offveq	$⊢ φ \to F_{S}^{'} +_{f} G_{S}^{'} = S D (F +_{f} G)$
59	58	eqcomd	$⊢ φ \to S D (F +_{f} G) = F_{S}^{'} +_{f} G_{S}^{'}$

Metamath Proof Explorer

Theorem dvaddf

Proof