Theorem dvmptid 22967

Description: Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)

Hypothesis

Ref	Expression
dvmptid.1	|- ( ph -> S e. { RR , CC } )

Assertion

Ref	Expression
dvmptid	|- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )

Distinct variable groups:   ph, x   x, S

Proof of Theorem dvmptid

Step	Hyp	Ref	Expression
1		eqid 2462	. 2 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
2		dvmptid.1	. 2 |- ( ph -> S e. { RR , CC } )
3	1	cnfldtopon 21858	. . 3 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
4		toponmax 19998	. . 3 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
5	3, 4	mp1i 13	. 2 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
6		recnprss 22915	. . . 4 |- ( S e. { RR , CC } -> S C_ CC )
7	2, 6	syl 17	. . 3 |- ( ph -> S C_ CC )
8		df-ss 3430	. . 3 |- ( S C_ CC <-> ( S i^i CC ) = S )
9	7, 8	sylib 201	. 2 |- ( ph -> ( S i^i CC ) = S )
10		simpr 467	. 2 |- ( ( ph /\ x e. CC ) -> x e. CC )
11		1cnd 9690	. 2 |- ( ( ph /\ x e. CC ) -> 1 e. CC )
12		mptresid 5181	. . . . 5 |- ( x e. CC |-> x ) = ( _I |` CC )
13	12	oveq2i 6331	. . . 4 |- ( CC _D ( x e. CC |-> x ) ) = ( CC _D ( _I |` CC ) )
14		dvid 22928	. . . 4 |- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
15		fconstmpt 4900	. . . 4 |- ( CC X. { 1 } ) = ( x e. CC |-> 1 )
16	13, 14, 15	3eqtri 2488	. . 3 |- ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 )
17	16	a1i 11	. 2 |- ( ph -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
18	1, 2, 5, 9, 10, 11, 17	dvmptres3 22966	1 |- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   i^i cin 3415   C_ wss 3416   {csn 3980   {cpr 3982   |-> cmpt 4477   _I cid 4766   X. cxp 4854   |` cres 4858   ` cfv 5605  (class class class)co 6320   CCcc 9568   RRcr 9569   1c1 9571   TopOpenctopn 15375  ℂ_fldccnfld 19025  TopOnctopon 19973   _D cdv 22874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fi 7956  df-sup 7987  df-inf 7988  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-icc 11676  df-fz 11820  df-seq 12252  df-exp 12311  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-plusg 15258  df-mulr 15259  df-starv 15260  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-rest 15376  df-topn 15377  df-topgen 15397  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-fbas 19022  df-fg 19023  df-cnfld 19026  df-top 19976  df-bases 19977  df-topon 19978  df-topsp 19979  df-cld 20089  df-ntr 20090  df-cls 20091  df-nei 20169  df-lp 20207  df-perf 20208  df-cn 20298  df-cnp 20299  df-haus 20386  df-fil 20916  df-fm 21008  df-flim 21009  df-flf 21010  df-xms 21390  df-ms 21391  df-cncf 21965  df-limc 22877  df-dv 22878

This theorem is referenced by:  dvef  22988  dvsincos  22989  mvth  23000  dvlipcn  23002  dvivthlem1  23016  lhop2  23023  dvfsumle  23029  dvfsumabs  23031  dvfsumlem2  23035  dvtaylp  23381  taylthlem2  23385  pige3  23528  advlog  23655  advlogexp  23656  logtayl  23661  dvcxp1  23736  dvcxp2  23737  dvcncxp1  23739  loglesqrt  23754  dvatan  23917  lgamgulmlem2  24011  log2sumbnd  24438  dvasin  32074  areacirclem1  32078  lhe4.4ex1a  36723  expgrowthi  36727  expgrowth  36729  binomcxplemdvbinom  36747  dvsinax  37869  dvmptidg  37873  dvcosax  37884  itgiccshift  37943  itgperiod  37944  itgsbtaddcnst  37945  dirkeritg  38065  fourierdlem39  38110  fourierdlem56  38127  fourierdlem60  38131  fourierdlem61  38132  fourierdlem62  38133  etransclem46  38246