Metamath Proof Explorer


Theorem dvmptmul

Description: Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
dvmptadd.a โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ โ„‚ )
dvmptadd.b โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ต โˆˆ ๐‘‰ )
dvmptadd.da โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
dvmptadd.c โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ถ โˆˆ โ„‚ )
dvmptadd.d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ท โˆˆ ๐‘Š )
dvmptadd.dc โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ท ) )
Assertion dvmptmul ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ด ยท ๐ถ ) ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐ต ยท ๐ถ ) + ( ๐ท ยท ๐ด ) ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
2 dvmptadd.a โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ โ„‚ )
3 dvmptadd.b โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ต โˆˆ ๐‘‰ )
4 dvmptadd.da โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
5 dvmptadd.c โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ถ โˆˆ โ„‚ )
6 dvmptadd.d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ๐ท โˆˆ ๐‘Š )
7 dvmptadd.dc โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ท ) )
8 2 fmpttd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) : ๐‘‹ โŸถ โ„‚ )
9 5 fmpttd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) : ๐‘‹ โŸถ โ„‚ )
10 4 dmeqd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) )
11 3 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ต โˆˆ ๐‘‰ )
12 dmmptg โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ต โˆˆ ๐‘‰ โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) = ๐‘‹ )
13 11 12 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ต ) = ๐‘‹ )
14 10 13 eqtrd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ๐‘‹ )
15 7 dmeqd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ท ) )
16 6 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ท โˆˆ ๐‘Š )
17 dmmptg โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐‘‹ ๐ท โˆˆ ๐‘Š โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ท ) = ๐‘‹ )
18 16 17 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ท ) = ๐‘‹ )
19 15 18 eqtrd โŠข ( ๐œ‘ โ†’ dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = ๐‘‹ )
20 1 8 9 14 19 dvmulf โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) ) = ( ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆ˜f + ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) )
21 ovex โŠข ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆˆ V
22 21 dmex โŠข dom ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆˆ V
23 19 22 eqeltrrdi โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ V )
24 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) )
25 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) )
26 23 2 5 24 25 offval2 โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ด ยท ๐ถ ) ) )
27 26 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) ) = ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ด ยท ๐ถ ) ) ) )
28 ovexd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ V )
29 ovexd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ( ๐ท ยท ๐ด ) โˆˆ V )
30 23 3 5 4 25 offval2 โŠข ( ๐œ‘ โ†’ ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ต ยท ๐ถ ) ) )
31 23 6 2 7 24 offval2 โŠข ( ๐œ‘ โ†’ ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ท ยท ๐ด ) ) )
32 23 28 29 30 31 offval2 โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆ˜f + ( ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ถ ) ) โˆ˜f ยท ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐ต ยท ๐ถ ) + ( ๐ท ยท ๐ด ) ) ) )
33 20 27 32 3eqtr3d โŠข ( ๐œ‘ โ†’ ( ๐‘† D ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐ด ยท ๐ถ ) ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐ต ยท ๐ถ ) + ( ๐ท ยท ๐ด ) ) ) )