Metamath Proof Explorer

Theorem dvmulcncf

Description: A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmulcncf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmulcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvmulcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
dvmulcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
dvmulcncf.gdv ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion dvmulcncf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 dvmulcncf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmulcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvmulcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
4 dvmulcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
5 dvmulcncf.gdv ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
6 cncff ⊢ ( ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
7 fdm ⊢ ( ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐹 ) = 𝑋 )
8 4 6 7 3syl ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
9 cncff ⊢ ( ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
10 fdm ⊢ ( ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐺 ) = 𝑋 )
11 5 9 10 3syl ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
12 1 2 3 8 11 dvmulf ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) )
13 ax-resscn ⊢ ℝ ⊆ ℂ
14 sseq1 ⊢ ( 𝑆 = ℝ → ( 𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ ) )
15 13 14 mpbiri ⊢ ( 𝑆 = ℝ → 𝑆 ⊆ ℂ )
16 eqimss ⊢ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ )
17 15 16 pm3.2i ⊢ ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) )
18 elpri ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
19 1 18 syl ⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
20 pm3.44 ⊢ ( ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) ) → ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝑆 ⊆ ℂ ) )
21 17 19 20 mpsyl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
22 dvbsss ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
23 8 22 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
24 dvcn ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐺 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐺 ) = 𝑋 ) → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
25 21 3 23 11 24 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
26 4 25 mulcncff ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
27 dvcn ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝑋 ) → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
28 21 2 23 8 27 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
29 5 28 mulcncff ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
30 26 29 addcncff ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f + ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
31 12 30 eqeltrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )