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 e. { RR , CC } /\ A e. CC ) -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )

Proof

Step Hyp Ref Expression
1 fconst6g 
 |-  ( A e. CC -> ( CC X. { A } ) : CC --> CC )
2 1 anim2i 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( S e. { RR , CC } /\ ( CC X. { A } ) : CC --> CC ) )
3 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
4 c0ex 
 |-  0 e. _V
5 4 fconst 
 |-  ( CC X. { 0 } ) : CC --> { 0 }
6 5 fdmi 
 |-  dom ( CC X. { 0 } ) = CC
7 3 6 sseqtrrdi 
 |-  ( S e. { RR , CC } -> S C_ dom ( CC X. { 0 } ) )
8 7 adantr 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> S C_ dom ( CC X. { 0 } ) )
9 dvconst 
 |-  ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
10 9 adantl 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
11 10 dmeqd 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> dom ( CC _D ( CC X. { A } ) ) = dom ( CC X. { 0 } ) )
12 8 11 sseqtrrd 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> S C_ dom ( CC _D ( CC X. { A } ) ) )
13 ssid 
 |-  CC C_ CC
14 12 13 jctil 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( CC C_ CC /\ S C_ dom ( CC _D ( CC X. { A } ) ) ) )
15 dvres3 
 |-  ( ( ( S e. { RR , CC } /\ ( CC X. { A } ) : CC --> CC ) /\ ( CC C_ CC /\ S C_ dom ( CC _D ( CC X. { A } ) ) ) ) -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( ( CC _D ( CC X. { A } ) ) |` S ) )
16 2 14 15 syl2anc 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( ( CC _D ( CC X. { A } ) ) |` S ) )
17 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
18 3 17 syl 
 |-  ( S e. { RR , CC } -> ( ( CC X. { A } ) |` S ) = ( S X. { A } ) )
19 18 oveq2d 
 |-  ( S e. { RR , CC } -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( S _D ( S X. { A } ) ) )
20 19 adantr 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( S _D ( ( CC X. { A } ) |` S ) ) = ( S _D ( S X. { A } ) ) )
21 10 reseq1d 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( ( CC X. { 0 } ) |` S ) )
22 xpssres 
 |-  ( S C_ CC -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
23 3 22 syl 
 |-  ( S e. { RR , CC } -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
24 23 adantr 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( ( CC X. { 0 } ) |` S ) = ( S X. { 0 } ) )
25 21 24 eqtrd 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( ( CC _D ( CC X. { A } ) ) |` S ) = ( S X. { 0 } ) )
26 16 20 25 3eqtr3d 
 |-  ( ( S e. { RR , CC } /\ A e. CC ) -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )