Metamath Proof Explorer


Theorem dvmptco

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

Ref Expression
Hypotheses dvmptco.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
dvmptco.t โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ { โ„ , โ„‚ } )
dvmptco.a โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ ๐‘Œ )
dvmptco.b โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ต โˆˆ ๐‘‰ )
dvmptco.c โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) โ†’ ๐ถ โˆˆ โ„‚ )
dvmptco.d โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) โ†’ ๐ท โˆˆ ๐‘Š )
dvmptco.da โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
dvmptco.dc โŠข ( ๐œ‘ โ†’ ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) = ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ท ) )
dvmptco.e โŠข ( ๐‘ฆ = ๐ด โ†’ ๐ถ = ๐ธ )
dvmptco.f โŠข ( ๐‘ฆ = ๐ด โ†’ ๐ท = ๐น )
Assertion dvmptco ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ธ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐น ยท ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 dvmptco.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
2 dvmptco.t โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ { โ„ , โ„‚ } )
3 dvmptco.a โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ ๐‘Œ )
4 dvmptco.b โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ต โˆˆ ๐‘‰ )
5 dvmptco.c โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) โ†’ ๐ถ โˆˆ โ„‚ )
6 dvmptco.d โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) โ†’ ๐ท โˆˆ ๐‘Š )
7 dvmptco.da โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
8 dvmptco.dc โŠข ( ๐œ‘ โ†’ ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) = ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ท ) )
9 dvmptco.e โŠข ( ๐‘ฆ = ๐ด โ†’ ๐ถ = ๐ธ )
10 dvmptco.f โŠข ( ๐‘ฆ = ๐ด โ†’ ๐ท = ๐น )
11 5 fmpttd โŠข ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) : ๐‘Œ โŸถ โ„‚ )
12 3 fmpttd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) : ๐‘‹ โŸถ ๐‘Œ )
13 8 dmeqd โŠข ( ๐œ‘ โ†’ dom ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) = dom ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ท ) )
14 6 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ๐ท โˆˆ ๐‘Š )
15 dmmptg โŠข ( โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ๐ท โˆˆ ๐‘Š โ†’ dom ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ท ) = ๐‘Œ )
16 14 15 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ท ) = ๐‘Œ )
17 13 16 eqtrd โŠข ( ๐œ‘ โ†’ dom ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) = ๐‘Œ )
18 7 dmeqd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
19 4 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ต โˆˆ ๐‘‰ )
20 dmmptg โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ต โˆˆ ๐‘‰ โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) = ๐‘‹ )
21 19 20 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) = ๐‘‹ )
22 18 21 eqtrd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ๐‘‹ )
23 2 1 11 12 17 22 dvcof โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) = ( ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆ˜f ยท ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) )
24 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) )
25 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) = ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) )
26 3 24 25 9 fmptco โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ธ ) )
27 26 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) = ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ธ ) ) )
28 ovex โŠข ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆˆ V
29 28 dmex โŠข dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆˆ V
30 22 29 eqeltrrdi โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ V )
31 2 5 6 8 dvmptcl โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) โ†’ ๐ท โˆˆ โ„‚ )
32 8 31 fmpt3d โŠข ( ๐œ‘ โ†’ ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) : ๐‘Œ โŸถ โ„‚ )
33 fco โŠข ( ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) : ๐‘Œ โŸถ โ„‚ โˆง ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) : ๐‘‹ โŸถ ๐‘Œ ) โ†’ ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) : ๐‘‹ โŸถ โ„‚ )
34 32 12 33 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) : ๐‘‹ โŸถ โ„‚ )
35 3 24 8 10 fmptco โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐น ) )
36 35 feq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) : ๐‘‹ โŸถ โ„‚ โ†” ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐น ) : ๐‘‹ โŸถ โ„‚ ) )
37 34 36 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐น ) : ๐‘‹ โŸถ โ„‚ )
38 37 fvmptelcdm โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐น โˆˆ โ„‚ )
39 30 38 4 35 7 offval2 โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ D ( ๐‘ฆ โˆˆ ๐‘Œ โ†ฆ ๐ถ ) ) โˆ˜ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆ˜f ยท ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐น ยท ๐ต ) ) )
40 23 27 39 3eqtr3d โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ธ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐น ยท ๐ต ) ) )