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 24671

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 6870	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶):𝑌⟶ℂ)
5		dvmptco.a	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
6	5	fmpttd 6870	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌)
7		dvmptco.dc	. . . . 5 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))
8	7	dmeqd 5745	. . . 4 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = dom (𝑦 ∈ 𝑌 ↦ 𝐷))
9		dvmptco.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)
10	9	ralrimiva 3113	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊)
11		dmmptg 6071	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → dom (𝑦 ∈ 𝑌 ↦ 𝐷) = 𝑌)
13	8, 12	eqtrd 2793	. . 3 ⊢ (𝜑 → dom (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = 𝑌)
14		dvmptco.da	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
15	14	dmeqd 5745	. . . 4 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = dom (𝑥 ∈ 𝑋 ↦ 𝐵))
16		dvmptco.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
17	16	ralrimiva 3113	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉)
18		dmmptg 6071	. . . . 5 ⊢ (∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
19	17, 18	syl 17	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 𝐵) = 𝑋)
20	15, 19	eqtrd 2793	. . 3 ⊢ (𝜑 → dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = 𝑋)
21	1, 2, 4, 6, 13, 20	dvcof 24647	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))))
22		eqidd 2759	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴))
23		eqidd 2759	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑦 ∈ 𝑌 ↦ 𝐶))
24		dvmptco.e	. . . 4 ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)
25	5, 22, 23, 24	fmptco 6882	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐸))
26	25	oveq2d 7166	. 2 ⊢ (𝜑 → (𝑆 D ((𝑦 ∈ 𝑌 ↦ 𝐶) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)))
27		ovex 7183	. . . . 5 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
28	27	dmex 7621	. . . 4 ⊢ dom (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ V
29	20, 28	eqeltrrdi 2861	. . 3 ⊢ (𝜑 → 𝑋 ∈ V)
30	1, 3, 9, 7	dvmptcl 24658	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ ℂ)
31	7, 30	fmpt3d 6871	. . . . . 6 ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ)
32		fco 6516	. . . . . 6 ⊢ (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)):𝑌⟶ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
33	31, 6, 32	syl2anc 587	. . . . 5 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ)
34		dvmptco.f	. . . . . . 7 ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)
35	5, 22, 7, 34	fmptco 6882	. . . . . 6 ⊢ (𝜑 → ((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐹))
36	35	feq1d 6483	. . . . 5 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ))
37	33, 36	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐹):𝑋⟶ℂ)
38	37	fvmptelrn 6868	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)
39	29, 38, 16, 35, 14	offval2 7424	. 2 ⊢ (𝜑 → (((𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∘_f · (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
40	21, 26, 39	3eqtr3d 2801	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3070 Vcvv 3409 {cpr 4524 ↦ cmpt 5112 dom cdm 5524 ∘ ccom 5528 ⟶wf 6331 (class class class)co 7150 ∘_f cof 7403 ℂcc 10573 ℝcr 10574 · cmul 10580 D cdv 24562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653 ax-addf 10654 ax-mulf 10655

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-int 4839 df-iun 4885 df-iin 4886 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-se 5484 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-isom 6344 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7405 df-om 7580 df-1st 7693 df-2nd 7694 df-supp 7836 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-2o 8113 df-er 8299 df-map 8418 df-pm 8419 df-ixp 8480 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-fsupp 8867 df-fi 8908 df-sup 8939 df-inf 8940 df-oi 9007 df-card 9401 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-7 11742 df-8 11743 df-9 11744 df-n0 11935 df-z 12021 df-dec 12138 df-uz 12283 df-q 12389 df-rp 12431 df-xneg 12548 df-xadd 12549 df-xmul 12550 df-icc 12786 df-fz 12940 df-fzo 13083 df-seq 13419 df-exp 13480 df-hash 13741 df-cj 14506 df-re 14507 df-im 14508 df-sqrt 14642 df-abs 14643 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-mulr 16637 df-starv 16638 df-sca 16639 df-vsca 16640 df-ip 16641 df-tset 16642 df-ple 16643 df-ds 16645 df-unif 16646 df-hom 16647 df-cco 16648 df-rest 16754 df-topn 16755 df-0g 16773 df-gsum 16774 df-topgen 16775 df-pt 16776 df-prds 16779 df-xrs 16833 df-qtop 16838 df-imas 16839 df-xps 16841 df-mre 16915 df-mrc 16916 df-acs 16918 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-submnd 18023 df-mulg 18292 df-cntz 18514 df-cmn 18975 df-psmet 20158 df-xmet 20159 df-met 20160 df-bl 20161 df-mopn 20162 df-fbas 20163 df-fg 20164 df-cnfld 20167 df-top 21594 df-topon 21611 df-topsp 21633 df-bases 21646 df-cld 21719 df-ntr 21720 df-cls 21721 df-nei 21798 df-lp 21836 df-perf 21837 df-cn 21927 df-cnp 21928 df-haus 22015 df-tx 22262 df-hmeo 22455 df-fil 22546 df-fm 22638 df-flim 22639 df-flf 22640 df-xms 23022 df-ms 23023 df-tms 23024 df-cncf 23579 df-limc 24565 df-dv 24566

This theorem is referenced by: dvrecg 24672 dvexp3 24677 dvsincos 24680 dvlipcn 24693 lhop2 24714 itgsubstlem 24747 dvtaylp 25064 taylthlem2 25068 pige3ALT 25211 advlogexp 25345 logtayl 25350 dvcxp1 25428 dvcxp2 25429 dvcncxp1 25431 loglesqrt 25446 dvatan 25620 lgamgulmlem2 25714 logdivsum 26216 log2sumbnd 26227 itgexpif 32105 dvtan 35387 dvasin 35421 areacirclem1 35425 lcmineqlem8 39603 lcmineqlem12 39607 dvrelogpow2b 39634 aks4d1p1p6 39639 expgrowthi 41410 expgrowth 41412 binomcxplemdvbinom 41430 dvsinexp 42919 dvxpaek 42948 fourierdlem28 43143 fourierdlem39 43154 fourierdlem56 43170 fourierdlem60 43174 fourierdlem61 43175 etransclem46 43288

W3C validator