Theorem dvmptconst

Description: Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvmptconst.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvmptconst.a	⊢ ( 𝜑 → 𝐴 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
	dvmptconst.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	dvmptconst	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptconst.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvmptconst.a	⊢ ( 𝜑 → 𝐴 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		dvmptconst.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
5		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 0 ∈ ℝ )
6	1 3	dvmptc	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )
7		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8	7	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
9	8	a1i	⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
10		ax-resscn	⊢ ℝ ⊆ ℂ
11		sseq1	⊢ ( 𝑆 = ℝ → ( 𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ ) )
12	10 11	mpbiri	⊢ ( 𝑆 = ℝ → 𝑆 ⊆ ℂ )
13		eqimss	⊢ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ )
14	12 13	pm3.2i	⊢ ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) )
15		elpri	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
16	1 15	syl	⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
17		pm3.44	⊢ ( ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) ) → ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝑆 ⊆ ℂ ) )
18	14 16 17	mpsyl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
19		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
20	9 18 19	syl2anc	⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
21		toponss	⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) ∧ 𝐴 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → 𝐴 ⊆ 𝑆 )
22	20 2 21	syl2anc	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
23		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
24	1 4 5 6 22 23 7 2	dvmptres	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )