dvmulf

Description: The product 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	dvmulf	$⊢ φ \to S D (F \times_{f} G) = (F_{S}^{'} \times_{f} G) +_{f} (G_{S}^{'} \times_{f} F)$

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	2	adantr	$⊢ (φ \land x \in X) \to F : X ⟶ ℂ$
7		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
8	4 7	eqsstrrdi	$⊢ φ \to X \subseteq S$
9	8	adantr	$⊢ (φ \land x \in X) \to X \subseteq S$
10	3	adantr	$⊢ (φ \land x \in X) \to G : X ⟶ ℂ$
11	1	adantr	$⊢ (φ \land x \in X) \to S \in \{ℝ, ℂ\}$
12	4	eleq2d	$⊢ φ \to (x \in dom F_{S}^{'} \leftrightarrow x \in X)$
13	12	biimpar	$⊢ (φ \land x \in X) \to x \in dom F_{S}^{'}$
14	5	eleq2d	$⊢ φ \to (x \in dom G_{S}^{'} \leftrightarrow x \in X)$
15	14	biimpar	$⊢ (φ \land x \in X) \to x \in dom G_{S}^{'}$
16	6 9 10 9 11 13 15	dvmul	$⊢ (φ \land x \in X) \to {(F \times_{f} G)}_{S}^{'} (x) = F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x)$
17	16	mpteq2dva	$⊢ φ \to (x \in X ⟼ {(F \times_{f} G)}_{S}^{'} (x)) = (x \in X ⟼ F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x))$
18		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ$
19	1 18	syl	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ$
20		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
21	1 20	syl	$⊢ φ \to S \subseteq ℂ$
22		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
23	22	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
24	1 8	ssexd	$⊢ φ \to X \in V$
25		inidm	$⊢ X \cap X = X$
26	23 2 3 24 24 25	off	$⊢ φ \to (F \times_{f} G) : X ⟶ ℂ$
27	21 26 8	dvbss	$⊢ φ \to dom {(F \times_{f} G)}_{S}^{'} \subseteq X$
28	21	adantr	$⊢ (φ \land x \in X) \to S \subseteq ℂ$
29		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
30	1 29	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
31	30	adantr	$⊢ (φ \land x \in X) \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
32		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
33		funfvbrb	$⊢ Fun F_{S}^{'} \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
34	31 32 33	3syl	$⊢ (φ \land x \in X) \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
35	13 34	mpbid	$⊢ (φ \land x \in X) \to x F_{S}^{'} F_{S}^{'} (x)$
36		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
37	1 36	syl	$⊢ φ \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
38	37	adantr	$⊢ (φ \land x \in X) \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
39		ffun	$⊢ G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \to Fun G_{S}^{'}$
40		funfvbrb	$⊢ Fun G_{S}^{'} \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
41	38 39 40	3syl	$⊢ (φ \land x \in X) \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
42	15 41	mpbid	$⊢ (φ \land x \in X) \to x G_{S}^{'} G_{S}^{'} (x)$
43		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
44	6 9 10 9 28 35 42 43	dvmulbr	$⊢ (φ \land x \in X) \to x {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x))$
45		reldv	$⊢ Rel {(F \times_{f} G)}_{S}^{'}$
46	45	releldmi	$⊢ x {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x)) \to x \in dom {(F \times_{f} G)}_{S}^{'}$
47	44 46	syl	$⊢ (φ \land x \in X) \to x \in dom {(F \times_{f} G)}_{S}^{'}$
48	27 47	eqelssd	$⊢ φ \to dom {(F \times_{f} G)}_{S}^{'} = X$
49	48	feq2d	$⊢ φ \to ({(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ \leftrightarrow {(F \times_{f} G)}_{S}^{'} : X ⟶ ℂ)$
50	19 49	mpbid	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} : X ⟶ ℂ$
51	50	feqmptd	$⊢ φ \to S D (F \times_{f} G) = (x \in X ⟼ {(F \times_{f} G)}_{S}^{'} (x))$
52		ovexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) G (x) \in V$
53		ovexd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) F (x) \in V$
54		fvexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in V$
55		fvexd	$⊢ (φ \land x \in X) \to G (x) \in V$
56	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
57	30 56	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
58	57	feqmptd	$⊢ φ \to S D F = (x \in X ⟼ F_{S}^{'} (x))$
59	3	feqmptd	$⊢ φ \to G = (x \in X ⟼ G (x))$
60	24 54 55 58 59	offval2	$⊢ φ \to F_{S}^{'} \times_{f} G = (x \in X ⟼ F_{S}^{'} (x) G (x))$
61		fvexd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) \in V$
62		fvexd	$⊢ (φ \land x \in X) \to F (x) \in V$
63	5	feq2d	$⊢ φ \to (G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \leftrightarrow G_{S}^{'} : X ⟶ ℂ)$
64	37 63	mpbid	$⊢ φ \to G_{S}^{'} : X ⟶ ℂ$
65	64	feqmptd	$⊢ φ \to S D G = (x \in X ⟼ G_{S}^{'} (x))$
66	2	feqmptd	$⊢ φ \to F = (x \in X ⟼ F (x))$
67	24 61 62 65 66	offval2	$⊢ φ \to G_{S}^{'} \times_{f} F = (x \in X ⟼ G_{S}^{'} (x) F (x))$
68	24 52 53 60 67	offval2	$⊢ φ \to (F_{S}^{'} \times_{f} G) +_{f} (G_{S}^{'} \times_{f} F) = (x \in X ⟼ F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x))$
69	17 51 68	3eqtr4d	$⊢ φ \to S D (F \times_{f} G) = (F_{S}^{'} \times_{f} G) +_{f} (G_{S}^{'} \times_{f} F)$

Metamath Proof Explorer

Theorem dvmulf

Proof