Metamath Proof Explorer


Theorem dvsid

Description: Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015)

Ref Expression
Assertion dvsid S S D I S = S × 1

Proof

Step Hyp Ref Expression
1 fnresi I Fn
2 rnresi ran I =
3 2 eqimssi ran I
4 df-f I : I Fn ran I
5 1 3 4 mpbir2an I :
6 5 jctr S S I :
7 recnprss S S
8 dvid D I = × 1
9 8 dmeqi dom I = dom × 1
10 1ex 1 V
11 10 fconst × 1 : 1
12 11 fdmi dom × 1 =
13 9 12 eqtri dom I =
14 7 13 sseqtrrdi S S dom I
15 ssid
16 14 15 jctil S S dom I
17 dvres3 S I : S dom I S D I S = I S
18 6 16 17 syl2anc S S D I S = I S
19 7 resabs1d S I S = I S
20 19 oveq2d S S D I S = S D I S
21 8 reseq1i I S = × 1 S
22 xpssres S × 1 S = S × 1
23 21 22 syl5eq S I S = S × 1
24 7 23 syl S I S = S × 1
25 18 20 24 3eqtr3d S S D I S = S × 1