Metamath Proof Explorer

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 · 𝐹 ) ) )