![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvmptres | Structured version Visualization version GIF version |
Description: Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
dvmptadd.s | ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
dvmptadd.a | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
dvmptadd.b | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) |
dvmptadd.da | ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) |
dvmptres.y | ⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
dvmptres.j | ⊢ 𝐽 = (𝐾 ↾t 𝑆) |
dvmptres.k | ⊢ 𝐾 = (TopOpen‘ℂfld) |
dvmptres.t | ⊢ (𝜑 → 𝑌 ∈ 𝐽) |
Ref | Expression |
---|---|
dvmptres | ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvmptadd.s | . 2 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | |
2 | dvmptadd.a | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) | |
3 | dvmptadd.b | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) | |
4 | dvmptadd.da | . 2 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) | |
5 | dvmptres.y | . 2 ⊢ (𝜑 → 𝑌 ⊆ 𝑋) | |
6 | dvmptres.j | . 2 ⊢ 𝐽 = (𝐾 ↾t 𝑆) | |
7 | dvmptres.k | . 2 ⊢ 𝐾 = (TopOpen‘ℂfld) | |
8 | 7 | cnfldtop 22919 | . . . . 5 ⊢ 𝐾 ∈ Top |
9 | resttop 21297 | . . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝑆 ∈ {ℝ, ℂ}) → (𝐾 ↾t 𝑆) ∈ Top) | |
10 | 8, 1, 9 | sylancr 582 | . . . 4 ⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ Top) |
11 | 6, 10 | syl5eqel 2886 | . . 3 ⊢ (𝜑 → 𝐽 ∈ Top) |
12 | dvmptres.t | . . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐽) | |
13 | isopn3i 21219 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝐽) → ((int‘𝐽)‘𝑌) = 𝑌) | |
14 | 11, 12, 13 | syl2anc 580 | . 2 ⊢ (𝜑 → ((int‘𝐽)‘𝑌) = 𝑌) |
15 | 1, 2, 3, 4, 5, 6, 7, 14 | dvmptres2 24070 | 1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ⊆ wss 3773 {cpr 4374 ↦ cmpt 4926 ‘cfv 6105 (class class class)co 6882 ℂcc 10226 ℝcr 10227 ↾t crest 16400 TopOpenctopn 16401 ℂfldccnfld 20072 Topctop 21030 intcnt 21154 D cdv 23972 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2379 ax-ext 2781 ax-rep 4968 ax-sep 4979 ax-nul 4987 ax-pow 5039 ax-pr 5101 ax-un 7187 ax-cnex 10284 ax-resscn 10285 ax-1cn 10286 ax-icn 10287 ax-addcl 10288 ax-addrcl 10289 ax-mulcl 10290 ax-mulrcl 10291 ax-mulcom 10292 ax-addass 10293 ax-mulass 10294 ax-distr 10295 ax-i2m1 10296 ax-1ne0 10297 ax-1rid 10298 ax-rnegex 10299 ax-rrecex 10300 ax-cnre 10301 ax-pre-lttri 10302 ax-pre-lttrn 10303 ax-pre-ltadd 10304 ax-pre-mulgt0 10305 ax-pre-sup 10306 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2593 df-eu 2611 df-clab 2790 df-cleq 2796 df-clel 2799 df-nfc 2934 df-ne 2976 df-nel 3079 df-ral 3098 df-rex 3099 df-reu 3100 df-rmo 3101 df-rab 3102 df-v 3391 df-sbc 3638 df-csb 3733 df-dif 3776 df-un 3778 df-in 3780 df-ss 3787 df-pss 3789 df-nul 4120 df-if 4282 df-pw 4355 df-sn 4373 df-pr 4375 df-tp 4377 df-op 4379 df-uni 4633 df-int 4672 df-iun 4716 df-iin 4717 df-br 4848 df-opab 4910 df-mpt 4927 df-tr 4950 df-id 5224 df-eprel 5229 df-po 5237 df-so 5238 df-fr 5275 df-we 5277 df-xp 5322 df-rel 5323 df-cnv 5324 df-co 5325 df-dm 5326 df-rn 5327 df-res 5328 df-ima 5329 df-pred 5902 df-ord 5948 df-on 5949 df-lim 5950 df-suc 5951 df-iota 6068 df-fun 6107 df-fn 6108 df-f 6109 df-f1 6110 df-fo 6111 df-f1o 6112 df-fv 6113 df-riota 6843 df-ov 6885 df-oprab 6886 df-mpt2 6887 df-om 7304 df-1st 7405 df-2nd 7406 df-wrecs 7649 df-recs 7711 df-rdg 7749 df-1o 7803 df-oadd 7807 df-er 7986 df-map 8101 df-pm 8102 df-en 8200 df-dom 8201 df-sdom 8202 df-fin 8203 df-fi 8563 df-sup 8594 df-inf 8595 df-pnf 10369 df-mnf 10370 df-xr 10371 df-ltxr 10372 df-le 10373 df-sub 10562 df-neg 10563 df-div 10981 df-nn 11317 df-2 11380 df-3 11381 df-4 11382 df-5 11383 df-6 11384 df-7 11385 df-8 11386 df-9 11387 df-n0 11585 df-z 11671 df-dec 11788 df-uz 11935 df-q 12038 df-rp 12079 df-xneg 12197 df-xadd 12198 df-xmul 12199 df-fz 12585 df-seq 13060 df-exp 13119 df-cj 14184 df-re 14185 df-im 14186 df-sqrt 14320 df-abs 14321 df-struct 16190 df-ndx 16191 df-slot 16192 df-base 16194 df-plusg 16284 df-mulr 16285 df-starv 16286 df-tset 16290 df-ple 16291 df-ds 16293 df-unif 16294 df-rest 16402 df-topn 16403 df-topgen 16423 df-psmet 20064 df-xmet 20065 df-met 20066 df-bl 20067 df-mopn 20068 df-cnfld 20073 df-top 21031 df-topon 21048 df-topsp 21070 df-bases 21083 df-cld 21156 df-ntr 21157 df-cls 21158 df-cnp 21365 df-xms 22457 df-ms 22458 df-limc 23975 df-dv 23976 |
This theorem is referenced by: dvmptfsum 24083 dvexp3 24086 dvlipcn 24102 dvivthlem1 24116 lhop2 24123 dvfsumle 24129 dvfsumabs 24131 dvfsumlem2 24135 taylthlem2 24473 pserdvlem2 24527 advlog 24745 advlogexp 24746 logtayl 24751 loglesqrt 24847 dvatan 25018 log2sumbnd 25589 dvtan 33952 dvasin 33988 dvacos 33989 areacirclem1 33992 dvmptconst 40877 dvmptidg 40879 itgsin0pilem1 40913 itgsbtaddcnst 40945 fourierdlem56 41126 fourierdlem60 41130 fourierdlem61 41131 fourierdlem62 41132 |
Copyright terms: Public domain | W3C validator |