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