dvmptres2 - Metamath Proof Explorer

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

Theorem dvmptres2 25923

Description: Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)

**Hypotheses**
Ref	Expression
dvmptadd.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
dvmptadd.a	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
dvmptadd.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
dvmptadd.da	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
dvmptres2.z	⊢ (𝜑 → 𝑍 ⊆ 𝑋)
dvmptres2.j	⊢ 𝐽 = (𝐾 ↾_t 𝑆)
dvmptres2.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
dvmptres2.i	⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌)

**Assertion**
Ref	Expression
dvmptres2	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))

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

**Proof of Theorem dvmptres2**
Step	Hyp	Ref	Expression
1		dvmptadd.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
2		recnprss 25862	. . . 4 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
4		dvmptadd.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
5	4	fmpttd 7110	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ)
6		dvmptadd.da	. . . . . 6 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
7	6	dmeqd 5890	. . . . 5 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
8		dvmptadd.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
9	8	ralrimiva 3133	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
10		dmmptg 6236	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
11	9, 10	syl 17	. . . . 5 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
12	7, 11	eqtrd 2771	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
13		dvbsss 25860	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ⊆ 𝑆
14	12, 13	eqsstrrdi 4009	. . 3 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
15		dvmptres2.z	. . . 4 ⊢ (𝜑 → 𝑍 ⊆ 𝑋)
16	15, 14	sstrd 3974	. . 3 ⊢ (𝜑 → 𝑍 ⊆ 𝑆)
17		dvmptres2.k	. . . 4 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
18		dvmptres2.j	. . . 4 ⊢ 𝐽 = (𝐾 ↾_t 𝑆)
19	17, 18	dvres 25869	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) ∧ (𝑋 ⊆ 𝑆 ∧ 𝑍 ⊆ 𝑆)) → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
20	3, 5, 14, 16, 19	syl22anc 838	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
21	15	resmptd 6032	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍) = (𝑥 ∈ 𝑍 ↦ 𝐴))
22	21	oveq2d 7426	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)))
23	6	reseq1d 5970	. . 3 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)))
24		dvmptres2.i	. . . 4 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌)
25	24	reseq2d 5971	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌))
26	17	cnfldtopon 24726	. . . . . . . . . 10 ⊢ 𝐾 ∈ (TopOn‘ℂ)
27		resttopon 23104	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
28	26, 3, 27	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
29	18, 28	eqeltrid 2839	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑆))
30		topontop 22856	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝐽 ∈ Top)
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
32		toponuni 22857	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝐽)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = ∪ 𝐽)
34	16, 33	sseqtrd 4000	. . . . . . 7 ⊢ (𝜑 → 𝑍 ⊆ ∪ 𝐽)
35		eqid 2736	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
36	35	ntrss2 23000	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑍 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
37	31, 34, 36	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
38	24, 37	eqsstrrd 3999	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝑍)
39	38, 15	sstrd 3974	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
40	39	resmptd 6032	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌) = (𝑥 ∈ 𝑌 ↦ 𝐵))
41	23, 25, 40	3eqtrd 2775	. 2 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
42	20, 22, 41	3eqtr3d 2779	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3052 ⊆ wss 3931 {cpr 4608 ∪ cuni 4888 ↦ cmpt 5206 dom cdm 5659 ↾ cres 5661 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 ↾_t crest 17439 TopOpenctopn 17440 ℂ_fldccnfld 21320 Topctop 22836 TopOnctopon 22853 intcnt 22960 D cdv 25821

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-map 8847 df-pm 8848 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9428 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-fz 13530 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-struct 17171 df-slot 17206 df-ndx 17218 df-base 17234 df-plusg 17289 df-mulr 17290 df-starv 17291 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-rest 17441 df-topn 17442 df-topgen 17462 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-cnp 23171 df-xms 24264 df-ms 24265 df-limc 25824 df-dv 25825

This theorem is referenced by: dvmptres 25924 dvmptcmul 25925 rolle 25951 mvth 25954 itgpowd 26014 taylthlem1 26338 pige3ALT 26486 logccv 26629 lgamgulmlem2 26997 dvrelog2 42082 dvrelog3 42083 lhe4.4ex1a 44320 binomcxplemdvbinom 44344 binomcxplemnotnn0 44347 itgsinexplem1 45950 dirkeritg 46098 fourierdlem39 46142 etransclem46 46276

W3C validator