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 26224

Description: Restriction of a derivative. Note that our definition of derivative df-dv 26180 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 26183	. 2 ⊢ Rel (𝑆 D (𝐹 ↾ 𝐵))
2		relres 5996	. 2 ⊢ Rel ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))
3		simpll 779	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝑆 ⊆ ℂ)
4		simplr 781	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐹:𝐴⟶ℂ)
5		inss1 4182	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
6		fssres 6746	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℂ ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
7	4, 5, 6	sylancl 598	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ)
8		resres 5983	. . . . . . . . 9 ⊢ ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ (𝐴 ∩ 𝐵))
9		ffn 6707	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴)
10		fnresdm 6656	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
11	4, 9, 10	3syl 19	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐴) = 𝐹)
12	11	reseq1d 5969	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ 𝐴) ↾ 𝐵) = (𝐹 ↾ 𝐵))
13	8, 12	eqtr3id 2810	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐹 ↾ 𝐵))
14	13	feq1d 6689	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶ℂ ↔ (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ))
15	7, 14	mpbid 235	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ)
16		simprl 783	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → 𝐴 ⊆ 𝑆)
17	5, 16	sstrid 3942	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝐴 ∩ 𝐵) ⊆ 𝑆)
18	3, 15, 17	dvcl 26212	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦) → 𝑦 ∈ ℂ)
19	18	ex 418	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 → 𝑦 ∈ ℂ))
20	3, 4, 16	dvcl 26212	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ)
21	20	ex 418	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ))
22	21	adantld 496	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ))
23		dvres.k	. . . . . 6 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
24		dvres.t	. . . . . 6 ⊢ 𝑇 = (𝐾 ↾_t 𝑆)
25		eqid 2761	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))
26	3	adantr 486	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑆 ⊆ ℂ)
27	4	adantr 486	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐹:𝐴⟶ℂ)
28	16	adantr 486	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐴 ⊆ 𝑆)
29		simplrr 790	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝐵 ⊆ 𝑆)
30		simpr 490	. . . . . 6 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
31	23, 24, 25, 26, 27, 28, 29, 30	dvreslem 26222	. . . . 5 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) ∧ 𝑦 ∈ ℂ) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
32	31	ex 418	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑦 ∈ ℂ → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))))
33	19, 22, 32	pm5.21ndd 382	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦)))
34		vex 3455	. . . 4 ⊢ 𝑦 ∈ V
35	34	brresi 5979	. . 3 ⊢ (𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))
36	33, 35	bitr4di 292	. 2 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ 𝑥((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))𝑦))
37	1, 2, 36	eqbrrdiv 5770	1 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑆 D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 ↾ cres 5653 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ℂcc 11191 − cmin 11534 / cdiv 11966 ↾_t crest 17584 TopOpenctopn 17585 ℂ_fldccnfld 21671 intcnt 23328 D cdv 26176

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 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

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 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fi 9396 df-sup 9427 df-inf 9428 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-fz 13633 df-seq 14138 df-exp 14198 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-struct 17318 df-slot 17353 df-ndx 17365 df-base 17381 df-plusg 17434 df-mulr 17435 df-starv 17436 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-rest 17586 df-topn 17587 df-topgen 17607 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-cnp 23539 df-xms 24632 df-ms 24633 df-limc 26179 df-dv 26180

This theorem is used by: dvmptresicc 26229 dvcmulf 26258 dvmptres2 26275 dvmptntr 26284 dvlip 26306 dvlipcn 26307 dvlip2 26308 c1liplem1 26309 dvgt0lem1 26315 dvne0 26324 lhop1lem 26326 lhop 26329 dvcnvrelem1 26330 dvcvx 26333 ftc2ditglem 26358 pserdv 26749 efcvx 26769 dvlog 26972 dvlog2 26974 ftc2re 35220 dvun 43390 dvresntr 46897 dvresioo 46900 dvbdfbdioolem1 46907 itgcoscmulx 46948 itgiccshift 46959 itgperiod 46960 dirkercncflem2 47083 fourierdlem57 47142 fourierdlem58 47143 fourierdlem72 47157 fourierdlem73 47158 fourierdlem74 47159 fourierdlem75 47160 fourierdlem80 47165 fourierdlem94 47179 fourierdlem103 47188 fourierdlem104 47189 fourierdlem113 47198

W3C validator