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 26024

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 25966	. . . 4 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
4		dvmptadd.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
5	4	fmpttd 7096	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ)
6		dvmptadd.da	. . . . . 6 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
7	6	dmeqd 5881	. . . . 5 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
8		dvmptadd.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
9	8	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
10		dmmptg 6229	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
11	9, 10	syl 17	. . . . 5 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
12	7, 11	eqtrd 2797	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
13		dvbsss 25964	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ⊆ 𝑆
14	12, 13	eqsstrrdi 3981	. . 3 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
15		dvmptres2.z	. . . 4 ⊢ (𝜑 → 𝑍 ⊆ 𝑋)
16	15, 14	sstrd 3946	. . 3 ⊢ (𝜑 → 𝑍 ⊆ 𝑆)
17		dvmptres2.k	. . . 4 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
18		dvmptres2.j	. . . 4 ⊢ 𝐽 = (𝐾 ↾_t 𝑆)
19	17, 18	dvres 25973	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) ∧ (𝑋 ⊆ 𝑆 ∧ 𝑍 ⊆ 𝑆)) → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
20	3, 5, 14, 16, 19	syl22anc 849	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)))
21	15	resmptd 6029	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍) = (𝑥 ∈ 𝑍 ↦ 𝐴))
22	21	oveq2d 7412	. 2 ⊢ (𝜑 → (𝑆 D ((𝑥 ∈ 𝑋 ↦ 𝐴) ↾ 𝑍)) = (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)))
23	6	reseq1d 5964	. . 3 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)))
24		dvmptres2.i	. . . 4 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌)
25	24	reseq2d 5965	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ ((int‘𝐽)‘𝑍)) = ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌))
26	17	cnfldtopon 24842	. . . . . . . . . 10 ⊢ 𝐾 ∈ (TopOn‘ℂ)
27		resttopon 23221	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
28	26, 3, 27	sylancr 596	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
29	18, 28	eqeltrid 2866	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑆))
30		topontop 22973	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝐽 ∈ Top)
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
32		toponuni 22974	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝐽)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = ∪ 𝐽)
34	16, 33	sseqtrd 3972	. . . . . . 7 ⊢ (𝜑 → 𝑍 ⊆ ∪ 𝐽)
35		eqid 2762	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
36	35	ntrss2 23117	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑍 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
37	31, 34, 36	syl2anc 593	. . . . . 6 ⊢ (𝜑 → ((int‘𝐽)‘𝑍) ⊆ 𝑍)
38	24, 37	eqsstrrd 3971	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝑍)
39	38, 15	sstrd 3946	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
40	39	resmptd 6029	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 𝐵) ↾ 𝑌) = (𝑥 ∈ 𝑌 ↦ 𝐵))
41	23, 25, 40	3eqtrd 2801	. 2 ⊢ (𝜑 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ↾ ((int‘𝐽)‘𝑍)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
42	20, 22, 41	3eqtr3d 2805	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ∀wral 3076 ⊆ wss 3904 {cpr 4584 ∪ cuni 4865 ↦ cmpt 5181 dom cdm 5647 ↾ cres 5649 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ℂcc 11071 ℝcr 11072 ↾_t crest 17449 TopOpenctopn 17450 ℂ_fldccnfld 21424 Topctop 22953 TopOnctopon 22970 intcnt 23077 D cdv 25925

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-er 8678 df-map 8810 df-pm 8811 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fi 9357 df-sup 9388 df-inf 9389 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-fz 13513 df-seq 14015 df-exp 14075 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-struct 17183 df-slot 17218 df-ndx 17230 df-base 17246 df-plusg 17299 df-mulr 17300 df-starv 17301 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-rest 17451 df-topn 17452 df-topgen 17472 df-psmet 21416 df-xmet 21417 df-met 21418 df-bl 21419 df-mopn 21420 df-cnfld 21425 df-top 22954 df-topon 22971 df-topsp 22993 df-bases 23006 df-cld 23079 df-ntr 23080 df-cls 23081 df-cnp 23288 df-xms 24380 df-ms 24381 df-limc 25928 df-dv 25929

This theorem is referenced by: dvmptres 26025 dvmptcmul 26026 rolle 26052 mvth 26054 itgpowd 26112 taylthlem1 26436 pige3ALT 26585 logccv 26728 lgamgulmlem2 27094 dvrelog2 42681 dvrelog3 42682 lhe4.4ex1a 44905 binomcxplemdvbinom 44929 binomcxplemnotnn0 44932 itgsinexplem1 46528 dirkeritg 46676 fourierdlem39 46720 etransclem46 46854

W3C validator