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