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

Metamath Proof Explorer

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 ) )