dvmptco - Metamath Proof Explorer

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

Theorem dvmptco 26285

Description: Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)

**Hypotheses**
Ref	Expression
dvmptco.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
dvmptco.t	⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})
dvmptco.a	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
dvmptco.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
dvmptco.c	⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ)
dvmptco.d	⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
dvmptco.da	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
dvmptco.dc	⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
dvmptco.e	⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
dvmptco.f	⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)

**Assertion**
Ref	Expression
dvmptco	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))

Distinct variable groups: 𝑦,𝐴 𝑥,𝐶 𝑥,𝐷 𝑦,𝐸 𝑦,𝐹 𝑦,𝑇 𝑥,𝑉 𝑥,𝑦,𝜑 𝑦,𝑊 𝑥,𝑋 𝑥,𝑌,𝑦 Allowed substitution hints: 𝐴(𝑥) 𝐵(𝑥, 𝑦) 𝐶(𝑦) 𝐷(𝑦) 𝑆(𝑥, 𝑦) 𝑇(𝑥) 𝐸(𝑥) 𝐹(𝑥) 𝑉(𝑦) 𝑊(𝑥) 𝑋(𝑦)

**Proof of Theorem dvmptco**
Step	Hyp	Ref	Expression
1		dvmptco.t	. . 3 ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})
2		dvmptco.s	. . 3 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
3		dvmptco.c	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ)
4	3	fmpttd 7113	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶):𝑌⟶ℂ)
5		dvmptco.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
6	5	fmpttd 7113	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌)
7		dvmptco.dc	. . . . 5 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
8	7	dmeqd 5887	. . . 4 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = dom (𝑦 ∈ 𝑌 ↦ 𝐷))
9		dvmptco.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
10	9	ralrimiva 3155	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊)
11		dmmptg 6242	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
12	10, 11	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
13	8, 12	eqtrd 2796	. . 3 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = 𝑌)
14		dvmptco.da	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
15	14	dmeqd 5887	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
16		dvmptco.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
17	16	ralrimiva 3155	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
18		dmmptg 6242	. . . . 5 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
19	17, 18	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
20	15, 19	eqtrd 2796	. . 3 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
21	1, 2, 4, 6, 13, 20	dvcof 26261	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))))
22		eqidd 2762	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴))
23		eqidd 2762	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑦 ∈ 𝑌 ↦ 𝐶))
24		dvmptco.e	. . . 4 ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
25	5, 22, 23, 24	fmptco 7128	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐸))
26	25	oveq2d 7434	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)))
27		ovex 7451	. . . . 5 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
28	27	dmex 7919	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
29	20, 28	eqeltrrdi 2870	. . 3 ⊢ (𝜑 → 𝑋 ∈ V)
30	1, 3, 9, 7	dvmptcl 26272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ ℂ)
31	7, 30	fmpt3d 7114	. . . . . 6 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ)
32		fco 6732	. . . . . 6 ⊢ (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
33	31, 6, 32	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
34		dvmptco.f	. . . . . . 7 ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)
35	5, 22, 7, 34	fmptco 7128	. . . . . 6 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐹))
36	35	feq1d 6689	. . . . 5 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ))
37	33, 36	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ)
38	37	fvmptelcdm 7111	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)
39	29, 38, 16, 35, 14	offval2 7711	. 2 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
40	21, 26, 39	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 Vcvv 3451 {cpr 4586 ↦ cmpt 5186 dom cdm 5651 ∘ ccom 5655 ⟶wf 6533 (class class class)co 7418 ∘_f cof 7689 ℂcc 11191 ℝcr 11192 · cmul 11198 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 ax-addf 11272

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-se 5605 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-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-card 10013 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-icc 13476 df-fz 13633 df-fzo 13782 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-mulg 19271 df-cntz 19524 df-cmn 19989 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 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-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-limc 26179 df-dv 26180

This theorem is used by: dvrecg 26286 dvexp3 26291 dvsincos 26294 dvlipcn 26307 lhop2 26328 itgsubstlem 26361 dvtaylp 26690 taylthlem2 26694 pige3ALT 26841 advlogexp 26976 logtayl 26981 dvcxp1 27061 dvcxp2 27062 dvcncxp1 27064 loglesqrt 27082 dvatan 27256 lgamgulmlem2 27350 logdivsum 27853 log2sumbnd 27864 itgexpif 35228 dvtan 38568 dvasin 38602 areacirclem1 38606 lcmineqlem8 43066 lcmineqlem12 43070 dvrelogpow2b 43098 aks4d1p1p6 43103 readvrec2 43392 readvrec 43393 readvcot 43395 expgrowthi 45302 expgrowth 45304 binomcxplemdvbinom 45322 dvsinexp 46890 dvxpaek 46919 fourierdlem28 47114 fourierdlem39 47125 fourierdlem56 47141 fourierdlem60 47145 fourierdlem61 47146 etransclem46 47259

W3C validator