dvmptntr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvmptntr		Structured version Visualization version GIF version

Theorem dvmptntr 25897

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)

**Hypotheses**
Ref	Expression
dvmptntr.s	⊢ (𝜑 → 𝑆 ⊆ ℂ)
dvmptntr.x	⊢ (𝜑 → 𝑋 ⊆ 𝑆)
dvmptntr.a	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
dvmptntr.j	⊢ 𝐽 = (𝐾 ↾_t 𝑆)
dvmptntr.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
dvmptntr.i	⊢ (𝜑 → ((int‘𝐽)‘𝑋) = 𝑌)

**Assertion**
Ref	Expression
dvmptntr	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)))

Distinct variable groups: 𝜑,𝑥 𝑥,𝑋 𝑥,𝑌 Allowed substitution hints: 𝐴(𝑥) 𝑆(𝑥) 𝐽(𝑥) 𝐾(𝑥)

**Proof of Theorem dvmptntr**
Step	Hyp	Ref	Expression
1		dvmptntr.j	. . . . . . . . 9 ⊢ 𝐽 = (𝐾 ↾_t 𝑆)
2		dvmptntr.k	. . . . . . . . . . 11 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
3	2	cnfldtopon 24692	. . . . . . . . . 10 ⊢ 𝐾 ∈ (TopOn‘ℂ)
4		dvmptntr.s	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
5		resttopon 23071	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
6	3, 4, 5	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
7	1, 6	eqeltrid 2835	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑆))
8		topontop 22823	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝐽 ∈ Top)
9	7, 8	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
10		dvmptntr.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
11		toponuni 22824	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝐽)
12	7, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = ∪ 𝐽)
13	10, 12	sseqtrd 3966	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ ∪ 𝐽)
14		eqid 2731	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
15	14	ntridm 22978	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ∪ 𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑋)) = ((int‘𝐽)‘𝑋))
16	9, 13, 15	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((int‘𝐽)‘((int‘𝐽)‘𝑋)) = ((int‘𝐽)‘𝑋))
17		dvmptntr.i	. . . . . . 7 ⊢ (𝜑 → ((int‘𝐽)‘𝑋) = 𝑌)
18	17	fveq2d 6821	. . . . . 6 ⊢ (𝜑 → ((int‘𝐽)‘((int‘𝐽)‘𝑋)) = ((int‘𝐽)‘𝑌))
19	16, 18	eqtr3d 2768	. . . . 5 ⊢ (𝜑 → ((int‘𝐽)‘𝑋) = ((int‘𝐽)‘𝑌))
20	19	reseq2d 5923	. . . 4 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑋)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑌)))
21		dvmptntr.a	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
22	21	fmpttd 7043	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ)
23	2, 1	dvres 25834	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) ∧ (𝑋 ⊆ 𝑆 ∧ 𝑋 ⊆ 𝑆)) → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑋)))
24	4, 22, 10, 10, 23	syl22anc 838	. . . 4 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑋)))
25	14	ntrss2 22967	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑋) ⊆ 𝑋)
26	9, 13, 25	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((int‘𝐽)‘𝑋) ⊆ 𝑋)
27	17, 26	eqsstrrd 3965	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
28	27, 10	sstrd 3940	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
29	2, 1	dvres 25834	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) ∧ (𝑋 ⊆ 𝑆 ∧ 𝑌 ⊆ 𝑆)) → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑌)))
30	4, 22, 10, 28, 29	syl22anc 838	. . . 4 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑌)))
31	20, 24, 30	3eqtr4d 2776	. . 3 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋)) = (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌)))
32		ssid 3952	. . . . 5 ⊢ 𝑋 ⊆ 𝑋
33		resmpt 5981	. . . . 5 ⊢ (𝑋 ⊆ 𝑋 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝐴))
34	32, 33	mp1i 13	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝐴))
35	34	oveq2d 7357	. . 3 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑋)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)))
36	31, 35	eqtr3d 2768	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)))
37	27	resmptd 5984	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌) = (𝑥 ∈ 𝑌 ↦ 𝐴))
38	37	oveq2d 7357	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑌)) = (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)))
39	36, 38	eqtr3d 2768	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ⊆ wss 3897 ∪ cuni 4854 ↦ cmpt 5167 ↾ cres 5613 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 ℂcc 10999 ↾_t crest 17319 TopOpenctopn 17320 ℂ_fldccnfld 21286 Topctop 22803 TopOnctopon 22820 intcnt 22927 D cdv 25786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-map 8747 df-pm 8748 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fi 9290 df-sup 9321 df-inf 9322 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-fz 13403 df-seq 13904 df-exp 13964 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-struct 17053 df-slot 17088 df-ndx 17100 df-base 17116 df-plusg 17169 df-mulr 17170 df-starv 17171 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-rest 17321 df-topn 17322 df-topgen 17342 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-cnp 23138 df-xms 24230 df-ms 24231 df-limc 25789 df-dv 25790

This theorem is referenced by: rolle 25916 cmvth 25917 cmvthOLD 25918 dvlip 25920 dvlipcn 25921 dvle 25934 dvfsumabs 25951 ftc2 25973 itgparts 25976 itgsubstlem 25977 lgamgulmlem2 26962 ftc2nc 37742 areacirc 37753 itgsin0pilem1 45988 itgsbtaddcnst 46020

W3C validator