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	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2	1	recnperf	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Perf )
3	1	perfdvf	⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Perf → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
4	2 3	syl	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )