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 25852

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 7069	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶):𝑌⟶ℂ)
5		dvmptco.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
6	5	fmpttd 7069	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌)
7		dvmptco.dc	. . . . 5 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
8	7	dmeqd 5859	. . . 4 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = dom (𝑦 ∈ 𝑌 ↦ 𝐷))
9		dvmptco.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
10	9	ralrimiva 3125	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊)
11		dmmptg 6203	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
13	8, 12	eqtrd 2764	. . 3 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = 𝑌)
14		dvmptco.da	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
15	14	dmeqd 5859	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
16		dvmptco.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
17	16	ralrimiva 3125	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
18		dmmptg 6203	. . . . 5 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
19	17, 18	syl 17	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
20	15, 19	eqtrd 2764	. . 3 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
21	1, 2, 4, 6, 13, 20	dvcof 25828	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))))
22		eqidd 2730	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴))
23		eqidd 2730	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑦 ∈ 𝑌 ↦ 𝐶))
24		dvmptco.e	. . . 4 ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
25	5, 22, 23, 24	fmptco 7083	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐸))
26	25	oveq2d 7385	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)))
27		ovex 7402	. . . . 5 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
28	27	dmex 7865	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
29	20, 28	eqeltrrdi 2837	. . 3 ⊢ (𝜑 → 𝑋 ∈ V)
30	1, 3, 9, 7	dvmptcl 25839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ ℂ)
31	7, 30	fmpt3d 7070	. . . . . 6 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ)
32		fco 6694	. . . . . 6 ⊢ (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
33	31, 6, 32	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
34		dvmptco.f	. . . . . . 7 ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)
35	5, 22, 7, 34	fmptco 7083	. . . . . 6 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐹))
36	35	feq1d 6652	. . . . 5 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ))
37	33, 36	mpbid 232	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ)
38	37	fvmptelcdm 7067	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)
39	29, 38, 16, 35, 14	offval2 7653	. 2 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
40	21, 26, 39	3eqtr3d 2772	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3444 {cpr 4587 ↦ cmpt 5183 dom cdm 5631 ∘ ccom 5635 ⟶wf 6495 (class class class)co 7369 ∘_f cof 7631 ℂcc 11042 ℝcr 11043 · cmul 11049 D cdv 25740

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-fi 9338 df-sup 9369 df-inf 9370 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-icc 13289 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17361 df-topn 17362 df-0g 17380 df-gsum 17381 df-topgen 17382 df-pt 17383 df-prds 17386 df-xrs 17441 df-qtop 17446 df-imas 17447 df-xps 17449 df-mre 17523 df-mrc 17524 df-acs 17526 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19225 df-cmn 19688 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-top 22757 df-topon 22774 df-topsp 22796 df-bases 22809 df-cld 22882 df-ntr 22883 df-cls 22884 df-nei 22961 df-lp 22999 df-perf 23000 df-cn 23090 df-cnp 23091 df-haus 23178 df-tx 23425 df-hmeo 23618 df-fil 23709 df-fm 23801 df-flim 23802 df-flf 23803 df-xms 24184 df-ms 24185 df-tms 24186 df-cncf 24747 df-limc 25743 df-dv 25744

This theorem is referenced by: dvrecg 25853 dvexp3 25858 dvsincos 25861 dvlipcn 25875 lhop2 25896 itgsubstlem 25931 dvtaylp 26254 taylthlem2 26258 taylthlem2OLD 26259 pige3ALT 26405 advlogexp 26540 logtayl 26545 dvcxp1 26625 dvcxp2 26626 dvcncxp1 26628 loglesqrt 26647 dvatan 26821 lgamgulmlem2 26916 logdivsum 27420 log2sumbnd 27431 itgexpif 34570 dvtan 37637 dvasin 37671 areacirclem1 37675 lcmineqlem8 41997 lcmineqlem12 42001 dvrelogpow2b 42029 aks4d1p1p6 42034 readvrec2 42322 readvrec 42323 readvcot 42325 expgrowthi 44295 expgrowth 44297 binomcxplemdvbinom 44315 dvsinexp 45882 dvxpaek 45911 fourierdlem28 46106 fourierdlem39 46117 fourierdlem56 46133 fourierdlem60 46137 fourierdlem61 46138 etransclem46 46251

W3C validator