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 \left\{ℝ,ℂ\right\}\to F_S^{\prime }:\mathrm{dom}{F}_S^{\prime }⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	recnperf	$$⊢S\in \left\{ℝ,ℂ\right\}\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$
3	1	perfdvf	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Perf}\to F_S^{\prime }:\mathrm{dom}{F}_S^{\prime }⟶ℂ$$
4	2 3	syl	$$⊢S\in \left\{ℝ,ℂ\right\}\to F_S^{\prime }:\mathrm{dom}{F}_S^{\prime }⟶ℂ$$