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

Metamath Proof Explorer

Theorem dvmptid

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

Ref Expression
Hypothesis dvmptid.1 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
Assertion dvmptid ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ) = ( 𝑥 ∈ 𝑆 ↦ 1 ) )

Proof

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