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 26096

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 7108	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶):𝑌⟶ℂ)
5		dvmptco.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
6	5	fmpttd 7108	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌)
7		dvmptco.dc	. . . . 5 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
8	7	dmeqd 5893	. . . 4 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = dom (𝑦 ∈ 𝑌 ↦ 𝐷))
9		dvmptco.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
10	9	ralrimiva 3163	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊)
11		dmmptg 6240	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
12	10, 11	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
13	8, 12	eqtrd 2804	. . 3 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = 𝑌)
14		dvmptco.da	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
15	14	dmeqd 5893	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
16		dvmptco.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
17	16	ralrimiva 3163	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
18		dmmptg 6240	. . . . 5 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
19	17, 18	syl 18	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
20	15, 19	eqtrd 2804	. . 3 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
21	1, 2, 4, 6, 13, 20	dvcof 26072	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))))
22		eqidd 2770	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴))
23		eqidd 2770	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑦 ∈ 𝑌 ↦ 𝐶))
24		dvmptco.e	. . . 4 ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
25	5, 22, 23, 24	fmptco 7123	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐸))
26	25	oveq2d 7424	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)))
27		ovex 7441	. . . . 5 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
28	27	dmex 7902	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
29	20, 28	eqeltrrdi 2878	. . 3 ⊢ (𝜑 → 𝑋 ∈ V)
30	1, 3, 9, 7	dvmptcl 26083	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ ℂ)
31	7, 30	fmpt3d 7109	. . . . . 6 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ)
32		fco 6728	. . . . . 6 ⊢ (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
33	31, 6, 32	syl2anc 595	. . . . 5 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
34		dvmptco.f	. . . . . . 7 ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)
35	5, 22, 7, 34	fmptco 7123	. . . . . 6 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐹))
36	35	feq1d 6685	. . . . 5 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ))
37	33, 36	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ)
38	37	fvmptelcdm 7106	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)
39	29, 38, 16, 35, 14	offval2 7692	. 2 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
40	21, 26, 39	3eqtr3d 2812	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ∀wral 3085 Vcvv 3463 {cpr 4593 ↦ cmpt 5193 dom cdm 5659 ∘ ccom 5663 ⟶wf 6529 (class class class)co 7408 ∘_f cof 7670 ℂcc 11094 ℝcr 11095 · cmul 11101 D cdv 25987

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173 ax-pre-sup 11174 ax-addf 11175

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7672 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-card 9921 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-div 11868 df-nn 12230 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-6 12303 df-7 12304 df-8 12305 df-9 12306 df-n0 12501 df-z 12588 df-dec 12708 df-uz 12859 df-q 12969 df-rp 13013 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-icc 13375 df-fz 13532 df-fzo 13679 df-seq 14034 df-exp 14094 df-hash 14363 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-struct 17203 df-sets 17220 df-slot 17238 df-ndx 17250 df-base 17266 df-ress 17287 df-plusg 17319 df-mulr 17320 df-starv 17321 df-sca 17322 df-vsca 17323 df-ip 17324 df-tset 17325 df-ple 17326 df-ds 17328 df-unif 17329 df-hom 17330 df-cco 17331 df-rest 17471 df-topn 17472 df-0g 17490 df-gsum 17491 df-topgen 17492 df-pt 17493 df-prds 17496 df-xrs 17552 df-qtop 17557 df-imas 17558 df-xps 17560 df-mre 17634 df-mrc 17635 df-acs 17637 df-mgm 18694 df-sgrp 18773 df-mnd 18789 df-submnd 18838 df-mulg 19130 df-cntz 19383 df-cmn 19848 df-psmet 21479 df-xmet 21480 df-met 21481 df-bl 21482 df-mopn 21483 df-fbas 21484 df-fg 21485 df-cnfld 21488 df-top 23016 df-topon 23033 df-topsp 23055 df-bases 23068 df-cld 23141 df-ntr 23142 df-cls 23143 df-nei 23220 df-lp 23258 df-perf 23259 df-cn 23349 df-cnp 23350 df-haus 23437 df-tx 23684 df-hmeo 23877 df-fil 23968 df-fm 24060 df-flim 24061 df-flf 24062 df-xms 24442 df-ms 24443 df-tms 24444 df-cncf 25002 df-limc 25990 df-dv 25991

This theorem is referenced by: dvrecg 26097 dvexp3 26102 dvsincos 26105 dvlipcn 26118 lhop2 26139 itgsubstlem 26172 dvtaylp 26495 taylthlem2 26499 pige3ALT 26647 advlogexp 26782 logtayl 26787 dvcxp1 26867 dvcxp2 26868 dvcncxp1 26870 loglesqrt 26888 dvatan 27062 lgamgulmlem2 27156 logdivsum 27659 log2sumbnd 27670 itgexpif 34934 dvtan 38204 dvasin 38238 areacirclem1 38242 lcmineqlem8 42688 lcmineqlem12 42692 dvrelogpow2b 42720 aks4d1p1p6 42725 readvrec2 43005 readvrec 43006 readvcot 43008 expgrowthi 44928 expgrowth 44930 binomcxplemdvbinom 44948 dvsinexp 46510 dvxpaek 46539 fourierdlem28 46734 fourierdlem39 46745 fourierdlem56 46761 fourierdlem60 46765 fourierdlem61 46766 etransclem46 46879

W3C validator