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 ( ๐ฅ โ ๐ โฆ ( ๐ด ยท ๐ถ ) ) ) = ( ๐ฅ โ ๐ โฆ ( ( ๐ต ยท ๐ถ ) + ( ๐ท ยท ๐ด ) ) ) ) |