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 26282

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 26224	. . . 4 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
3	1, 2	syl 18	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
4		dvmptadd.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
5	4	fmpttd 7115	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ)
6		dvmptadd.da	. . . . . 6 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
7	6	dmeqd 5887	. . . . 5 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
8		dvmptadd.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
9	8	ralrimiva 3155	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
10		dmmptg 6243	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
11	9, 10	syl 18	. . . . 5 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
12	7, 11	eqtrd 2796	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
13		dvbsss 26222	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ⊆ 𝑆
14	12, 13	eqsstrrdi 3976	. . 3 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
15		dvmptres2.z	. . . 4 ⊢ (𝜑 → 𝑍 ⊆ 𝑋)
16	15, 14	sstrd 3941	. . 3 ⊢ (𝜑 → 𝑍 ⊆ 𝑆)
17		dvmptres2.k	. . . 4 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
18		dvmptres2.j	. . . 4 ⊢ 𝐽 = (𝐾 ↾_t 𝑆)
19	17, 18	dvres 26231	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) ∧ (𝑋 ⊆ 𝑆 ∧ 𝑍 ⊆ 𝑆)) → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
20	3, 5, 14, 16, 19	syl22anc 852	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
21	15	resmptd 6032	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍) = (𝑥 ∈ 𝑍 ↦ 𝐴))
22	21	oveq2d 7436	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)))
23	6	reseq1d 5969	. . 3 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)))
24		dvmptres2.i	. . . 4 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌)
25	24	reseq2d 5970	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌))
26	17	cnfldtopon 25101	. . . . . . . . . 10 ⊢ 𝐾 ∈ (TopOn‘ℂ)
27		resttopon 23479	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
28	26, 3, 27	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
29	18, 28	eqeltrid 2865	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑆))
30		topontop 23231	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝐽 ∈ Top)
31	29, 30	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
32		toponuni 23232	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝐽)
33	29, 32	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = ∪ 𝐽)
34	16, 33	sseqtrd 3967	. . . . . . 7 ⊢ (𝜑 → 𝑍 ⊆ ∪ 𝐽)
35		eqid 2761	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
36	35	ntrss2 23375	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑍 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
37	31, 34, 36	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
38	24, 37	eqsstrrd 3966	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝑍)
39	38, 15	sstrd 3941	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
40	39	resmptd 6032	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌) = (𝑥 ∈ 𝑌 ↦ 𝐵))
41	23, 25, 40	3eqtrd 2800	. 2 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
42	20, 22, 41	3eqtr3d 2804	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ⊆ wss 3899 {cpr 4586 ∪ cuni 4867 ↦ cmpt 5186 dom cdm 5651 ↾ cres 5653 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 ↾_t crest 17591 TopOpenctopn 17592 ℂ_fldccnfld 21678 Topctop 23211 TopOnctopon 23228 intcnt 23335 D cdv 26183

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-map 8849 df-pm 8850 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fi 9403 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-fz 13640 df-seq 14145 df-exp 14205 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-struct 17325 df-slot 17360 df-ndx 17372 df-base 17388 df-plusg 17441 df-mulr 17442 df-starv 17443 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-rest 17593 df-topn 17594 df-topgen 17614 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-cnfld 21679 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-cnp 23546 df-xms 24639 df-ms 24640 df-limc 26186 df-dv 26187

This theorem is used by: dvmptres 26283 dvmptcmul 26284 rolle 26310 mvth 26312 itgpowd 26370 taylthlem1 26700 pige3ALT 26848 logccv 26991 lgamgulmlem2 27357 dvrelog2 43114 dvrelog3 43115 lhe4.4ex1a 45312 binomcxplemdvbinom 45336 binomcxplemnotnn0 45339 itgsinexplem1 46963 dirkeritg 47111 fourierdlem39 47155 etransclem46 47289

W3C validator