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 26160

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 7114	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶):𝑌⟶ℂ)
5		dvmptco.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
6	5	fmpttd 7114	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌)
7		dvmptco.dc	. . . . 5 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
8	7	dmeqd 5897	. . . 4 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = dom (𝑦 ∈ 𝑌 ↦ 𝐷))
9		dvmptco.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
10	9	ralrimiva 3159	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊)
11		dmmptg 6245	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
12	10, 11	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
13	8, 12	eqtrd 2800	. . 3 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = 𝑌)
14		dvmptco.da	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
15	14	dmeqd 5897	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
16		dvmptco.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
17	16	ralrimiva 3159	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
18		dmmptg 6245	. . . . 5 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
19	17, 18	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
20	15, 19	eqtrd 2800	. . 3 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
21	1, 2, 4, 6, 13, 20	dvcof 26136	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))))
22		eqidd 2766	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴))
23		eqidd 2766	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑦 ∈ 𝑌 ↦ 𝐶))
24		dvmptco.e	. . . 4 ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
25	5, 22, 23, 24	fmptco 7129	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐸))
26	25	oveq2d 7432	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)))
27		ovex 7449	. . . . 5 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
28	27	dmex 7908	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
29	20, 28	eqeltrrdi 2874	. . 3 ⊢ (𝜑 → 𝑋 ∈ V)
30	1, 3, 9, 7	dvmptcl 26147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ ℂ)
31	7, 30	fmpt3d 7115	. . . . . 6 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ)
32		fco 6734	. . . . . 6 ⊢ (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
33	31, 6, 32	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
34		dvmptco.f	. . . . . . 7 ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)
35	5, 22, 7, 34	fmptco 7129	. . . . . 6 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐹))
36	35	feq1d 6691	. . . . 5 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ))
37	33, 36	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ)
38	37	fvmptelcdm 7112	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)
39	29, 38, 16, 35, 14	offval2 7700	. 2 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
40	21, 26, 39	3eqtr3d 2808	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3081 Vcvv 3457 {cpr 4593 ↦ cmpt 5194 dom cdm 5663 ∘ ccom 5667 ⟶wf 6536 (class class class)co 7416 ∘_f cof 7678 ℂcc 11109 ℝcr 11110 · cmul 11116 D cdv 26051

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189 ax-addf 11190

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9325 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-7 12319 df-8 12320 df-9 12321 df-n0 12516 df-z 12603 df-dec 12723 df-uz 12874 df-q 12984 df-rp 13028 df-xneg 13148 df-xadd 13149 df-xmul 13150 df-icc 13390 df-fz 13547 df-fzo 13695 df-seq 14051 df-exp 14111 df-hash 14380 df-cj 15169 df-re 15170 df-im 15171 df-sqrt 15305 df-abs 15306 df-struct 17224 df-sets 17241 df-slot 17259 df-ndx 17271 df-base 17287 df-ress 17308 df-plusg 17340 df-mulr 17341 df-starv 17342 df-sca 17343 df-vsca 17344 df-ip 17345 df-tset 17346 df-ple 17347 df-ds 17349 df-unif 17350 df-hom 17351 df-cco 17352 df-rest 17492 df-topn 17493 df-0g 17511 df-gsum 17512 df-topgen 17513 df-pt 17514 df-prds 17517 df-xrs 17573 df-qtop 17578 df-imas 17579 df-xps 17581 df-mre 17655 df-mrc 17656 df-acs 17658 df-mgm 18715 df-sgrp 18798 df-mnd 18814 df-submnd 18865 df-mulg 19157 df-cntz 19410 df-cmn 19875 df-psmet 21543 df-xmet 21544 df-met 21545 df-bl 21546 df-mopn 21547 df-fbas 21548 df-fg 21549 df-cnfld 21552 df-top 23080 df-topon 23097 df-topsp 23119 df-bases 23132 df-cld 23205 df-ntr 23206 df-cls 23207 df-nei 23284 df-lp 23322 df-perf 23323 df-cn 23413 df-cnp 23414 df-haus 23501 df-tx 23748 df-hmeo 23941 df-fil 24032 df-fm 24124 df-flim 24125 df-flf 24126 df-xms 24506 df-ms 24507 df-tms 24508 df-cncf 25066 df-limc 26054 df-dv 26055

This theorem is used by: dvrecg 26161 dvexp3 26166 dvsincos 26169 dvlipcn 26182 lhop2 26203 itgsubstlem 26236 dvtaylp 26562 taylthlem2 26566 pige3ALT 26714 advlogexp 26849 logtayl 26854 dvcxp1 26934 dvcxp2 26935 dvcncxp1 26937 loglesqrt 26955 dvatan 27129 lgamgulmlem2 27223 logdivsum 27726 log2sumbnd 27737 itgexpif 35017 dvtan 38354 dvasin 38388 areacirclem1 38392 lcmineqlem8 42836 lcmineqlem12 42840 dvrelogpow2b 42868 aks4d1p1p6 42873 readvrec2 43155 readvrec 43156 readvcot 43158 expgrowthi 45076 expgrowth 45078 binomcxplemdvbinom 45096 dvsinexp 46658 dvxpaek 46687 fourierdlem28 46882 fourierdlem39 46893 fourierdlem56 46909 fourierdlem60 46913 fourierdlem61 46914 etransclem46 47027

W3C validator