This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvfg

Description: Explicitly write out the functionality condition on derivative for S = RR and CC . (Contributed by Mario Carneiro, 9-Feb-2015)

		Ref	Expression
	Assertion	dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$

Step	Hyp	Ref	Expression
1		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
2	1	recnperf	$⊢ S \in \{ℝ, ℂ\} \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Perf$
3	1	perfdvf	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Perf \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
4	2 3	syl	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$