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 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
30 1 29 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
32 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
33 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
34 31 32 33 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
35 13 34 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
36 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
37 1 36 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
39 ffun ⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
40 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
41 38 39 40 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
42 15 41 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) )
43 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
44 6 9 10 9 28 35 42 43 dvmulbr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
45 reldv ⊢ Rel ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) )
46 45 releldmi ⊢ ( 𝑥 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
47 44 46 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
48 27 47 eqelssd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = 𝑋 )
49 48 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ ↔ ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : 𝑋 ⟶ ℂ ) )
50 19 49 mpbid ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : 𝑋 ⟶ ℂ )
51 50 feqmptd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑥 ) ) )
52 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ V )
53 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ V )
54 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ V )
55 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
56 4 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
57 30 56 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
58 57 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
59 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
60 24 54 55 58 59 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
61 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ∈ V )
62 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
63 5 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
64 37 63 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
65 64 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
66 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
67 24 61 62 65 66 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
68 24 52 53 60 67 offval2 ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ) )
69 17 51 68 3eqtr4d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) )