Theorem dvmptid 22468

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 2396	. 2 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
2		dvmptid.1	. 2 |- ( ph -> S e. { RR , CC } )
3	1	cnfldtopon 21398	. . 3 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
4		toponmax 19537	. . 3 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
5	3, 4	mp1i 12	. 2 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
6		recnprss 22416	. . . 4 |- ( S e. { RR , CC } -> S C_ CC )
7	2, 6	syl 16	. . 3 |- ( ph -> S C_ CC )
8		df-ss 3420	. . 3 |- ( S C_ CC <-> ( S i^i CC ) = S )
9	7, 8	sylib 196	. 2 |- ( ph -> ( S i^i CC ) = S )
10		simpr 459	. 2 |- ( ( ph /\ x e. CC ) -> x e. CC )
11		1cnd 9545	. 2 |- ( ( ph /\ x e. CC ) -> 1 e. CC )
12		mptresid 5257	. . . . 5 |- ( x e. CC |-> x ) = ( _I |` CC )
13	12	oveq2i 6229	. . . 4 |- ( CC _D ( x e. CC |-> x ) ) = ( CC _D ( _I |` CC ) )
14		dvid 22429	. . . 4 |- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
15		fconstmpt 4974	. . . 4 |- ( CC X. { 1 } ) = ( x e. CC |-> 1 )
16	13, 14, 15	3eqtri 2429	. . 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 22467	1 |- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399   e. wcel 1836   i^i cin 3405   C_ wss 3406   {csn 3961   {cpr 3963   |-> cmpt 4442   _I cid 4721   X. cxp 4928   |` cres 4932   ` cfv 5513  (class class class)co 6218   CCcc 9423   RRcr 9424   1c1 9426   TopOpenctopn 14852  ℂ_fldccnfld 18556  TopOnctopon 19503   _D cdv 22375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502  ax-pre-sup 9503

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-iin 4263  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-map 7362  df-pm 7363  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-fi 7808  df-sup 7838  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-div 10146  df-nn 10475  df-2 10533  df-3 10534  df-4 10535  df-5 10536  df-6 10537  df-7 10538  df-8 10539  df-9 10540  df-10 10541  df-n0 10735  df-z 10804  df-dec 10918  df-uz 11024  df-q 11124  df-rp 11162  df-xneg 11261  df-xadd 11262  df-xmul 11263  df-icc 11479  df-fz 11616  df-seq 12034  df-exp 12093  df-cj 12957  df-re 12958  df-im 12959  df-sqrt 13093  df-abs 13094  df-struct 14659  df-ndx 14660  df-slot 14661  df-base 14662  df-plusg 14738  df-mulr 14739  df-starv 14740  df-tset 14744  df-ple 14745  df-ds 14747  df-unif 14748  df-rest 14853  df-topn 14854  df-topgen 14874  df-psmet 18547  df-xmet 18548  df-met 18549  df-bl 18550  df-mopn 18551  df-fbas 18552  df-fg 18553  df-cnfld 18557  df-top 19507  df-bases 19509  df-topon 19510  df-topsp 19511  df-cld 19628  df-ntr 19629  df-cls 19630  df-nei 19708  df-lp 19746  df-perf 19747  df-cn 19837  df-cnp 19838  df-haus 19925  df-fil 20455  df-fm 20547  df-flim 20548  df-flf 20549  df-xms 20931  df-ms 20932  df-cncf 21490  df-limc 22378  df-dv 22379

This theorem is referenced by:  dvef  22489  dvsincos  22490  mvth  22501  dvlipcn  22503  dvivthlem1  22517  lhop2  22524  dvfsumle  22530  dvfsumabs  22532  dvfsumlem2  22536  dvtaylp  22873  taylthlem2  22877  pige3  23018  advlog  23145  advlogexp  23146  logtayl  23151  dvcxp1  23226  dvcxp2  23227  loglesqrt  23242  dvatan  23405  log2sumbnd  23869  lgamgulmlem2  28801  dvcncxp1  30306  dvasin  30309  areacirclem1  30313  lhe4.4ex1a  31442  expgrowthi  31446  expgrowth  31448  binomcxplemdvbinom  31466  dvsinax  31913  dvmptidg  31917  dvcosax  31928  itgiccshift  31984  itgperiod  31985  itgsbtaddcnst  31986  dirkeritg  32089  fourierdlem39  32133  fourierdlem56  32150  fourierdlem60  32154  fourierdlem61  32155  fourierdlem62  32156  etransclem46  32268