![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvmptid | Structured version Visualization version GIF version |
Description: Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
dvmptid.1 | ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
Ref | Expression |
---|---|
dvmptid | ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝑥)) = (𝑥 ∈ 𝑆 ↦ 1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2773 | . 2 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld) | |
2 | dvmptid.1 | . 2 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | |
3 | 1 | cnfldtopon 23110 | . . 3 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ) |
4 | toponmax 21254 | . . 3 ⊢ ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld)) | |
5 | 3, 4 | mp1i 13 | . 2 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂfld)) |
6 | recnprss 24221 | . . . 4 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) | |
7 | 2, 6 | syl 17 | . . 3 ⊢ (𝜑 → 𝑆 ⊆ ℂ) |
8 | df-ss 3838 | . . 3 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆) | |
9 | 7, 8 | sylib 210 | . 2 ⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆) |
10 | simpr 477 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) | |
11 | 1cnd 10433 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ) | |
12 | mptresid 5760 | . . . . 5 ⊢ (𝑥 ∈ ℂ ↦ 𝑥) = ( I ↾ ℂ) | |
13 | 12 | oveq2i 6986 | . . . 4 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (ℂ D ( I ↾ ℂ)) |
14 | dvid 24234 | . . . 4 ⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1}) | |
15 | fconstmpt 5461 | . . . 4 ⊢ (ℂ × {1}) = (𝑥 ∈ ℂ ↦ 1) | |
16 | 13, 14, 15 | 3eqtri 2801 | . . 3 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1) |
17 | 16 | a1i 11 | . 2 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
18 | 1, 2, 5, 9, 10, 11, 17 | dvmptres3 24272 | 1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝑥)) = (𝑥 ∈ 𝑆 ↦ 1)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 ∩ cin 3823 ⊆ wss 3824 {csn 4436 {cpr 4438 ↦ cmpt 5005 I cid 5308 × cxp 5402 ↾ cres 5406 ‘cfv 6186 (class class class)co 6975 ℂcc 10332 ℝcr 10333 1c1 10335 TopOpenctopn 16550 ℂfldccnfld 20263 TopOnctopon 21238 D cdv 24180 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-rep 5046 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 ax-cnex 10390 ax-resscn 10391 ax-1cn 10392 ax-icn 10393 ax-addcl 10394 ax-addrcl 10395 ax-mulcl 10396 ax-mulrcl 10397 ax-mulcom 10398 ax-addass 10399 ax-mulass 10400 ax-distr 10401 ax-i2m1 10402 ax-1ne0 10403 ax-1rid 10404 ax-rnegex 10405 ax-rrecex 10406 ax-cnre 10407 ax-pre-lttri 10408 ax-pre-lttrn 10409 ax-pre-ltadd 10410 ax-pre-mulgt0 10411 ax-pre-sup 10412 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-nel 3069 df-ral 3088 df-rex 3089 df-reu 3090 df-rmo 3091 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-pss 3840 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-tp 4441 df-op 4443 df-uni 4710 df-int 4747 df-iun 4791 df-iin 4792 df-br 4927 df-opab 4989 df-mpt 5006 df-tr 5028 df-id 5309 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-we 5365 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6936 df-ov 6978 df-oprab 6979 df-mpo 6980 df-om 7396 df-1st 7500 df-2nd 7501 df-wrecs 7749 df-recs 7811 df-rdg 7849 df-1o 7904 df-oadd 7908 df-er 8088 df-map 8207 df-pm 8208 df-en 8306 df-dom 8307 df-sdom 8308 df-fin 8309 df-fi 8669 df-sup 8700 df-inf 8701 df-pnf 10475 df-mnf 10476 df-xr 10477 df-ltxr 10478 df-le 10479 df-sub 10671 df-neg 10672 df-div 11098 df-nn 11439 df-2 11502 df-3 11503 df-4 11504 df-5 11505 df-6 11506 df-7 11507 df-8 11508 df-9 11509 df-n0 11707 df-z 11793 df-dec 11911 df-uz 12058 df-q 12162 df-rp 12204 df-xneg 12323 df-xadd 12324 df-xmul 12325 df-icc 12560 df-fz 12708 df-seq 13184 df-exp 13244 df-cj 14318 df-re 14319 df-im 14320 df-sqrt 14454 df-abs 14455 df-struct 16340 df-ndx 16341 df-slot 16342 df-base 16344 df-plusg 16433 df-mulr 16434 df-starv 16435 df-tset 16439 df-ple 16440 df-ds 16442 df-unif 16443 df-rest 16551 df-topn 16552 df-topgen 16572 df-psmet 20255 df-xmet 20256 df-met 20257 df-bl 20258 df-mopn 20259 df-fbas 20260 df-fg 20261 df-cnfld 20264 df-top 21222 df-topon 21239 df-topsp 21261 df-bases 21274 df-cld 21347 df-ntr 21348 df-cls 21349 df-nei 21426 df-lp 21464 df-perf 21465 df-cn 21555 df-cnp 21556 df-haus 21643 df-fil 22174 df-fm 22266 df-flim 22267 df-flf 22268 df-xms 22649 df-ms 22650 df-cncf 23205 df-limc 24183 df-dv 24184 |
This theorem is referenced by: dvef 24296 dvsincos 24297 mvth 24308 dvlipcn 24310 dvivthlem1 24324 lhop2 24331 dvfsumle 24337 dvfsumabs 24339 dvfsumlem2 24343 dvtaylp 24677 taylthlem2 24681 pige3ALT 24824 advlog 24954 advlogexp 24955 logtayl 24960 dvcxp1 25038 dvcxp2 25039 dvcncxp1 25041 loglesqrt 25056 dvatan 25230 lgamgulmlem2 25325 log2sumbnd 25838 itgexpif 31558 dvasin 34452 areacirclem1 34456 lhe4.4ex1a 40111 expgrowthi 40115 expgrowth 40117 binomcxplemdvbinom 40135 dvsinax 41657 dvmptidg 41661 dvcosax 41671 itgiccshift 41725 itgperiod 41726 itgsbtaddcnst 41727 dirkeritg 41848 fourierdlem39 41892 fourierdlem56 41908 fourierdlem60 41912 fourierdlem61 41913 fourierdlem62 41914 etransclem46 42026 |
Copyright terms: Public domain | W3C validator |