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 24980

Description: Restriction of a derivative. Note that our definition of derivative df-dv 24936 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 24939	. 2 ⊢ Rel (𝑆 D (𝐹 ↾ 𝐵))
2		relres 5909	. 2 ⊢ Rel ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))
3		simpll 763	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝑆 ⊆ ℂ)
4		simplr 765	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐹:𝐴⟶ℂ)
5		inss1 4159	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
6		fssres 6624	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℂ ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
7	4, 5, 6	sylancl 585	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
8		resres 5893	. . . . . . . . 9 ⊢ ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ (𝐴 ∩ 𝐵))
9		ffn 6584	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴)
10		fnresdm 6535	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
11	4, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐴) = 𝐹)
12	11	reseq1d 5879	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ 𝐵))
13	8, 12	eqtr3id 2793	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐹 ↾ 𝐵))
14	13	feq1d 6569	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ ↔ (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ))
15	7, 14	mpbid 231	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ)
16		simprl 767	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐴 ⊆ 𝑆)
17	5, 16	sstrid 3928	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐴 ∩ 𝐵) ⊆ 𝑆)
18	3, 15, 17	dvcl 24968	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦) → 𝑦 ∈ ℂ)
19	18	ex 412	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 → 𝑦 ∈ ℂ))
20	3, 4, 16	dvcl 24968	. . . . . 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 2738	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))
26	3	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑆 ⊆ ℂ)
27	4	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐹:𝐴⟶ℂ)
28	16	adantr 480	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐴 ⊆ 𝑆)
29		simplrr 774	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐵 ⊆ 𝑆)
30		simpr 484	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
31	23, 24, 25, 26, 27, 28, 29, 30	dvreslem 24978	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
32	31	ex 412	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑦 ∈ ℂ → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))))
33	19, 22, 32	pm5.21ndd 380	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
34		vex 3426	. . . 4 ⊢ 𝑦 ∈ V
35	34	brresi 5889	. . 3 ⊢ (𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))
36	33, 35	bitr4di 288	. 2 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ 𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦))
37	1, 2, 36	eqbrrdiv 5693	1 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑆 D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∖ cdif 3880 ∩ cin 3882 ⊆ wss 3883 {csn 4558 class class class wbr 5070 ↦ cmpt 5153 ↾ cres 5582 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 − cmin 11135 / cdiv 11562 ↾_t crest 17048 TopOpenctopn 17049 ℂ_fldccnfld 20510 intcnt 22076 D cdv 24932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fi 9100 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-fz 13169 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-struct 16776 df-slot 16811 df-ndx 16823 df-base 16841 df-plusg 16901 df-mulr 16902 df-starv 16903 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-rest 17050 df-topn 17051 df-topgen 17071 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-cnp 22287 df-xms 23381 df-ms 23382 df-limc 24935 df-dv 24936

This theorem is referenced by: dvmptresicc 24985 dvcmulf 25014 dvmptres2 25031 dvmptntr 25040 dvlip 25062 dvlipcn 25063 dvlip2 25064 c1liplem1 25065 dvgt0lem1 25071 dvne0 25080 lhop1lem 25082 lhop 25085 dvcnvrelem1 25086 dvcvx 25089 ftc2ditglem 25114 pserdv 25493 efcvx 25513 dvlog 25711 dvlog2 25713 ftc2re 32478 dvresntr 43349 dvresioo 43352 dvbdfbdioolem1 43359 itgcoscmulx 43400 itgiccshift 43411 itgperiod 43412 dirkercncflem2 43535 fourierdlem57 43594 fourierdlem58 43595 fourierdlem72 43609 fourierdlem73 43610 fourierdlem74 43611 fourierdlem75 43612 fourierdlem80 43617 fourierdlem94 43631 fourierdlem103 43640 fourierdlem104 43641 fourierdlem113 43650

W3C validator