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	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmulcncf.f	$$⊢\phi \to F:X⟶ℂ$$
	dvmulcncf.g	$$⊢\phi \to G:X⟶ℂ$$
	dvmulcncf.fdv	$$⊢\phi \to F_S^{\prime }:X\underset{cn}{⟶}ℂ$$
	dvmulcncf.gdv	$$⊢\phi \to G_S^{\prime }:X\underset{cn}{⟶}ℂ$$
Assertion	dvmulcncf	$$⊢\phi \to {\left(F{\times }_{f}G\right)}_S^{\prime }:X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dvmulcncf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmulcncf.f	$$⊢\phi \to F:X⟶ℂ$$
3		dvmulcncf.g	$$⊢\phi \to G:X⟶ℂ$$
4		dvmulcncf.fdv	$$⊢\phi \to F_S^{\prime }:X\underset{cn}{⟶}ℂ$$
5		dvmulcncf.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	dvmulf	$$⊢\phi \to S\mathrm{D}\left(F{\times }_{f}G\right)=\left(F_S^{\prime }{\times }_{f}G\right){+}_f\left(G_S^{\prime }{\times }_{f}F\right)$$
13		ax-resscn	$$⊢ℝ\subseteq ℂ$$
14		sseq1	$$⊢S=ℝ\to \left(S\subseteq ℂ\leftrightarrow ℝ\subseteq ℂ\right)$$
15	13 14	mpbiri	$$⊢S=ℝ\to S\subseteq ℂ$$
16		eqimss	$$⊢S=ℂ\to S\subseteq ℂ$$
17	15 16	pm3.2i	$$⊢\left(\left(S=ℝ\to S\subseteq ℂ\right)\wedge \left(S=ℂ\to S\subseteq ℂ\right)\right)$$
18		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
19	1 18	syl	$$⊢\phi \to \left(S=ℝ\vee S=ℂ\right)$$
20		pm3.44	$$⊢\left(\left(S=ℝ\to S\subseteq ℂ\right)\wedge \left(S=ℂ\to S\subseteq ℂ\right)\right)\to \left(\left(S=ℝ\vee S=ℂ\right)\to S\subseteq ℂ\right)$$
21	17 19 20	mpsyl	$$⊢\phi \to S\subseteq ℂ$$
22		dvbsss	$$⊢\mathrm{dom}{F}_S^{\prime }\subseteq S$$
23	8 22	eqsstrrdi	$$⊢\phi \to X\subseteq S$$
24		dvcn	$$⊢\left(\left(S\subseteq ℂ\wedge G:X⟶ℂ\wedge X\subseteq S\right)\wedge \mathrm{dom}{G}_S^{\prime }=X\right)\to G:X\underset{cn}{⟶}ℂ$$
25	21 3 23 11 24	syl31anc	$$⊢\phi \to G:X\underset{cn}{⟶}ℂ$$
26	4 25	mulcncff	$$⊢\phi \to \left(F_S^{\prime }{\times }_{f}G\right):X\underset{cn}{⟶}ℂ$$
27		dvcn	$$⊢\left(\left(S\subseteq ℂ\wedge F:X⟶ℂ\wedge X\subseteq S\right)\wedge \mathrm{dom}{F}_S^{\prime }=X\right)\to F:X\underset{cn}{⟶}ℂ$$
28	21 2 23 8 27	syl31anc	$$⊢\phi \to F:X\underset{cn}{⟶}ℂ$$
29	5 28	mulcncff	$$⊢\phi \to \left(G_S^{\prime }{\times }_{f}F\right):X\underset{cn}{⟶}ℂ$$
30	26 29	addcncff	$$⊢\phi \to \left(\left(F_S^{\prime }{\times }_{f}G\right){+}_f\left(G_S^{\prime }{\times }_{f}F\right)\right):X\underset{cn}{⟶}ℂ$$
31	12 30	eqeltrd	$$⊢\phi \to {\left(F{\times }_{f}G\right)}_S^{\prime }:X\underset{cn}{⟶}ℂ$$