dvres - Metamath Proof Explorer

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

Theorem dvres 25834

Description: Restriction of a derivative. Note that our definition of derivative df-dv 25790 would still make sense if we demanded that 𝑥 be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point 𝑥 when restricted to different subsets containing 𝑥; a classic example is the absolute value function restricted to [0, +∞) and (-∞, 0]. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)

**Hypotheses**
Ref	Expression
dvres.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
dvres.t	⊢ 𝑇 = (𝐾 ↾_t 𝑆)

**Assertion**
Ref	Expression
dvres	⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑆 D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵)))

Proof of Theorem dvres Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldv 25793	. 2 ⊢ Rel (𝑆 D (𝐹 ↾ 𝐵))
2		relres 5949	. 2 ⊢ Rel ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))
3		simpll 766	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝑆 ⊆ ℂ)
4		simplr 768	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐹:𝐴⟶ℂ)
5		inss1 4182	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
6		fssres 6684	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℂ ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
7	4, 5, 6	sylancl 586	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
8		resres 5936	. . . . . . . . 9 ⊢ ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ (𝐴 ∩ 𝐵))
9		ffn 6646	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴)
10		fnresdm 6595	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
11	4, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐴) = 𝐹)
12	11	reseq1d 5922	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ 𝐵))
13	8, 12	eqtr3id 2780	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐹 ↾ 𝐵))
14	13	feq1d 6628	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ ↔ (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ))
15	7, 14	mpbid 232	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ)
16		simprl 770	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐴 ⊆ 𝑆)
17	5, 16	sstrid 3941	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐴 ∩ 𝐵) ⊆ 𝑆)
18	3, 15, 17	dvcl 25822	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦) → 𝑦 ∈ ℂ)
19	18	ex 412	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 → 𝑦 ∈ ℂ))
20	3, 4, 16	dvcl 25822	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ)
21	20	ex 412	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ))
22	21	adantld 490	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ))
23		dvres.k	. . . . . 6 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
24		dvres.t	. . . . . 6 ⊢ 𝑇 = (𝐾 ↾_t 𝑆)
25		eqid 2731	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))
26	3	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑆 ⊆ ℂ)
27	4	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐹:𝐴⟶ℂ)
28	16	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐴 ⊆ 𝑆)
29		simplrr 777	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐵 ⊆ 𝑆)
30		simpr 484	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
31	23, 24, 25, 26, 27, 28, 29, 30	dvreslem 25832	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
32	31	ex 412	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑦 ∈ ℂ → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))))
33	19, 22, 32	pm5.21ndd 379	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
34		vex 3440	. . . 4 ⊢ 𝑦 ∈ V
35	34	brresi 5932	. . 3 ⊢ (𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))
36	33, 35	bitr4di 289	. 2 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ 𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦))
37	1, 2, 36	eqbrrdiv 5729	1 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑆 D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ∖ cdif 3894 ∩ cin 3896 ⊆ wss 3897 {csn 4571 class class class wbr 5086 ↦ cmpt 5167 ↾ cres 5613 Fn wfn 6471 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 ℂcc 10999 − cmin 11339 / cdiv 11769 ↾_t crest 17319 TopOpenctopn 17320 ℂ_fldccnfld 21286 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: dvmptresicc 25839 dvcmulf 25870 dvmptres2 25888 dvmptntr 25897 dvlip 25920 dvlipcn 25921 dvlip2 25922 c1liplem1 25923 dvgt0lem1 25929 dvne0 25938 lhop1lem 25940 lhop 25943 dvcnvrelem1 25944 dvcvx 25947 ftc2ditglem 25974 pserdv 26361 efcvx 26381 dvlog 26582 dvlog2 26584 ftc2re 34603 dvun 42392 dvresntr 45956 dvresioo 45959 dvbdfbdioolem1 45966 itgcoscmulx 46007 itgiccshift 46018 itgperiod 46019 dirkercncflem2 46142 fourierdlem57 46201 fourierdlem58 46202 fourierdlem72 46216 fourierdlem73 46217 fourierdlem74 46218 fourierdlem75 46219 fourierdlem80 46224 fourierdlem94 46238 fourierdlem103 46247 fourierdlem104 46248 fourierdlem113 46257

W3C validator