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