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

Metamath Proof Explorer

Theorem dvmptidg

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

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

Proof

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