dvsubcncf

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

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

Metamath Proof Explorer