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		fvexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in V$
30		fvexd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) \in V$
31		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
32	1 31	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
33	32	adantr	$⊢ (φ \land x \in X) \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
34		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
35		funfvbrb	$⊢ Fun F_{S}^{'} \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
36	33 34 35	3syl	$⊢ (φ \land x \in X) \to (x \in dom F_{S}^{'} \leftrightarrow x F_{S}^{'} F_{S}^{'} (x))$
37	13 36	mpbid	$⊢ (φ \land x \in X) \to x F_{S}^{'} F_{S}^{'} (x)$
38		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
39	1 38	syl	$⊢ φ \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
40	39	adantr	$⊢ (φ \land x \in X) \to G_{S}^{'} : 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	40 41 42	3syl	$⊢ (φ \land x \in X) \to (x \in dom G_{S}^{'} \leftrightarrow x G_{S}^{'} G_{S}^{'} (x))$
44	15 43	mpbid	$⊢ (φ \land x \in X) \to x G_{S}^{'} G_{S}^{'} (x)$
45		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
46	6 9 10 9 28 29 30 37 44 45	dvmulbr	$⊢ (φ \land x \in X) \to x {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (x) G (x) + G_{S}^{'} (x) F (x))$
47		reldv	$⊢ Rel {(F \times_{f} G)}_{S}^{'}$
48	47	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}^{'}$
49	46 48	syl	$⊢ (φ \land x \in X) \to x \in dom {(F \times_{f} G)}_{S}^{'}$
50	27 49	eqelssd	$⊢ φ \to dom {(F \times_{f} G)}_{S}^{'} = X$
51	50	feq2d	$⊢ φ \to ({(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ \leftrightarrow {(F \times_{f} G)}_{S}^{'} : X ⟶ ℂ)$
52	19 51	mpbid	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} : X ⟶ ℂ$
53	52	feqmptd	$⊢ φ \to S D (F \times_{f} G) = (x \in X ⟼ {(F \times_{f} G)}_{S}^{'} (x))$
54		ovexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) G (x) \in V$
55		ovexd	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) F (x) \in V$
56		fvexd	$⊢ (φ \land x \in X) \to G (x) \in V$
57	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
58	32 57	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
59	58	feqmptd	$⊢ φ \to S D F = (x \in X ⟼ F_{S}^{'} (x))$
60	3	feqmptd	$⊢ φ \to G = (x \in X ⟼ G (x))$
61	24 29 56 59 60	offval2	$⊢ φ \to F_{S}^{'} \times_{f} G = (x \in X ⟼ F_{S}^{'} (x) G (x))$
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	39 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 30 62 65 66	offval2	$⊢ φ \to G_{S}^{'} \times_{f} F = (x \in X ⟼ G_{S}^{'} (x) F (x))$
68	24 54 55 61 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 53 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