Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvaddf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	dvaddf.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
	dvaddf.df	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
	dvaddf.dg	⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
Assertion	dvmulf	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvaddf.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvaddf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3		dvaddf.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
4		dvaddf.df	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
5		dvaddf.dg	⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ℂ )
7		dvbsss	⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
8	4 7	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ⊆ 𝑆 )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 : 𝑋 ⟶ ℂ )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ { ℝ , ℂ } )
12	4	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ∈ 𝑋 ) )
13	12	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐹 ) )
14	5	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ∈ 𝑋 ) )
15	14	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D 𝐺 ) )
16	6 9 10 9 11 13 15	dvmul	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑥 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
17	16	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ) )
18		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ )
19	1 18	syl	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ )
20		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
21	1 20	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
22		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
23	22	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
24	1 8	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
25		inidm	⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
26	23 2 3 24 24 25	off	⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) : 𝑋 ⟶ ℂ )
27	21 26 8	dvbss	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⊆ 𝑋 )
28	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ⊆ ℂ )
29		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ V )
30		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ∈ V )
31		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
32	1 31	syl	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
34		ffun	⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
35		funfvbrb	⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
36	33 34 35	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
37	13 36	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
38		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
39	1 38	syl	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
41		ffun	⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
42		funfvbrb	⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
43	40 41 42	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
44	15 43	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
45		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
46	6 9 10 9 28 29 30 37 44 45	dvmulbr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
47		reldv	⊢ Rel ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) )
48	47	releldmi	⊢ ( 𝑥 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
49	46 48	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
50	27 49	eqelssd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = 𝑋 )
51	50	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ ↔ ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : 𝑋 ⟶ ℂ ) )
52	19 51	mpbid	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : 𝑋 ⟶ ℂ )
53	52	feqmptd	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑥 ) ) )
54		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ V )
55		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ V )
56		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
57	4	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
58	32 57	mpbid	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
59	58	feqmptd	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
60	3	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
61	24 29 56 59 60	offval2	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
62		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
63	5	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
64	39 63	mpbid	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
65	64	feqmptd	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
66	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
67	24 30 62 65 66	offval2	⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
68	24 54 55 61 67	offval2	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ) )
69	17 53 68	3eqtr4d	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) )