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

Metamath Proof Explorer

Theorem dvmptc

Description: Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptid.1 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptc.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
Assertion dvmptc ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )

Proof

Step Hyp Ref Expression
1 dvmptid.1 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptc.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 3 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
5 toponmax ⊢ ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) → ℂ ∈ ( TopOpen ‘ ℂfld ) )
6 4 5 mp1i ⊢ ( 𝜑 → ℂ ∈ ( TopOpen ‘ ℂfld ) )
7 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
8 1 7 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
9 dfss2 ⊢ ( 𝑆 ⊆ ℂ ↔ ( 𝑆 ∩ ℂ ) = 𝑆 )
10 8 9 sylib ⊢ ( 𝜑 → ( 𝑆 ∩ ℂ ) = 𝑆 )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
12 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℂ )
13 dvconst ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
14 2 13 syl ⊢ ( 𝜑 → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
15 fconstmpt ⊢ ( ℂ × { 𝐴 } ) = ( 𝑥 ∈ ℂ ↦ 𝐴 )
16 15 oveq2i ⊢ ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐴 ) )
17 fconstmpt ⊢ ( ℂ × { 0 } ) = ( 𝑥 ∈ ℂ ↦ 0 )
18 14 16 17 3eqtr3g ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
19 3 1 6 10 11 12 18 dvmptres3 ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )