Theorem dvsubcncf

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

	Ref	Expression
Hypotheses	dvsubcncf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvsubcncf.f	$$⊢\phi \to F:X⟶ℂ$$
	dvsubcncf.g	$$⊢\phi \to G:X⟶ℂ$$
	dvsubcncf.fdv	$$⊢\phi \to F_S^{\prime }:X\underset{cn}{⟶}ℂ$$
	dvsubcncf.gdv	$$⊢\phi \to G_S^{\prime }:X\underset{cn}{⟶}ℂ$$
Assertion	dvsubcncf	$$⊢\phi \to {\left(F{-}_{f}G\right)}_S^{\prime }:X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dvsubcncf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvsubcncf.f	$$⊢\phi \to F:X⟶ℂ$$
3		dvsubcncf.g	$$⊢\phi \to G:X⟶ℂ$$
4		dvsubcncf.fdv	$$⊢\phi \to F_S^{\prime }:X\underset{cn}{⟶}ℂ$$
5		dvsubcncf.gdv	$$⊢\phi \to G_S^{\prime }:X\underset{cn}{⟶}ℂ$$
6		cncff	$$⊢F_S^{\prime }:X\underset{cn}{⟶}ℂ\to F_S^{\prime }:X⟶ℂ$$
7		fdm	$$⊢F_S^{\prime }:X⟶ℂ\to \mathrm{dom}{F}_S^{\prime }=X$$
8	4 6 7	3syl	$$⊢\phi \to \mathrm{dom}{F}_S^{\prime }=X$$
9		cncff	$$⊢G_S^{\prime }:X\underset{cn}{⟶}ℂ\to G_S^{\prime }:X⟶ℂ$$
10		fdm	$$⊢G_S^{\prime }:X⟶ℂ\to \mathrm{dom}{G}_S^{\prime }=X$$
11	5 9 10	3syl	$$⊢\phi \to \mathrm{dom}{G}_S^{\prime }=X$$
12	1 2 3 8 11	dvsubf	$$⊢\phi \to S\mathrm{D}\left(F{-}_{f}G\right)=F_S^{\prime }{-}_f{G}_S^{\prime }$$
13	4 5	subcncff	$$⊢\phi \to \left(F_S^{\prime }{-}_f{G}_S^{\prime }\right):X\underset{cn}{⟶}ℂ$$
14	12 13	eqeltrd	$$⊢\phi \to {\left(F{-}_{f}G\right)}_S^{\prime }:X\underset{cn}{⟶}ℂ$$