Metamath Proof Explorer

Theorem dvsconst

Description: Derivative of a constant function on the real or complex numbers. The function may return a complex A even if S is RR . (Contributed by Steve Rodriguez, 11-Nov-2015)

Ref Expression
Assertion dvsconst ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S D S × A = S × 0

Proof

Step Hyp Ref Expression
1 fconst6g ⊢ A ∈ ℂ → ℂ × A : ℂ ⟶ ℂ
2 1 anim2i ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S ∈ ℝ ℂ ∧ ℂ × A : ℂ ⟶ ℂ
3 recnprss ⊢ S ∈ ℝ ℂ → S ⊆ ℂ
4 c0ex ⊢ 0 ∈ V
5 4 fconst ⊢ ℂ × 0 : ℂ ⟶ 0
6 5 fdmi ⊢ dom ⁡ ℂ × 0 = ℂ
7 3 6 sseqtrrdi ⊢ S ∈ ℝ ℂ → S ⊆ dom ⁡ ℂ × 0
8 7 adantr ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S ⊆ dom ⁡ ℂ × 0
9 dvconst ⊢ A ∈ ℂ → ℂ D ℂ × A = ℂ × 0
10 9 adantl ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → ℂ D ℂ × A = ℂ × 0
11 10 dmeqd ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → dom ⁡ ℂ × A ℂ ′ = dom ⁡ ℂ × 0
12 8 11 sseqtrrd ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S ⊆ dom ⁡ ℂ × A ℂ ′
13 ssid ⊢ ℂ ⊆ ℂ
14 12 13 jctil ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → ℂ ⊆ ℂ ∧ S ⊆ dom ⁡ ℂ × A ℂ ′
15 dvres3 ⊢ S ∈ ℝ ℂ ∧ ℂ × A : ℂ ⟶ ℂ ∧ ℂ ⊆ ℂ ∧ S ⊆ dom ⁡ ℂ × A ℂ ′ → S D ℂ × A ↾ S = ℂ × A ℂ ′ ↾ S
16 2 14 15 syl2anc ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S D ℂ × A ↾ S = ℂ × A ℂ ′ ↾ S
17 xpssres ⊢ S ⊆ ℂ → ℂ × A ↾ S = S × A
18 3 17 syl ⊢ S ∈ ℝ ℂ → ℂ × A ↾ S = S × A
19 18 oveq2d ⊢ S ∈ ℝ ℂ → S D ℂ × A ↾ S = S D S × A
20 19 adantr ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S D ℂ × A ↾ S = S D S × A
21 10 reseq1d ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → ℂ × A ℂ ′ ↾ S = ℂ × 0 ↾ S
22 xpssres ⊢ S ⊆ ℂ → ℂ × 0 ↾ S = S × 0
23 3 22 syl ⊢ S ∈ ℝ ℂ → ℂ × 0 ↾ S = S × 0
24 23 adantr ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → ℂ × 0 ↾ S = S × 0
25 21 24 eqtrd ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → ℂ × A ℂ ′ ↾ S = S × 0
26 16 20 25 3eqtr3d ⊢ S ∈ ℝ ℂ ∧ A ∈ ℂ → S D S × A = S × 0