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 ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐴 ∈ ℂ ) → ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = ( 𝑆 × { 0 } ) )

Proof

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