Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.5 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
2 | | itgmulc2nc.7 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) |
3 | | elrege0 13372 |
. . . . . . . 8
โข (๐ต โ (0[,)+โ) โ
(๐ต โ โ โง 0
โค ๐ต)) |
4 | 1, 2, 3 | sylanbrc 584 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ (0[,)+โ)) |
5 | | 0e0icopnf 13376 |
. . . . . . . 8
โข 0 โ
(0[,)+โ) |
6 | 5 | a1i 11 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,)+โ)) |
7 | 4, 6 | ifclda 4522 |
. . . . . 6
โข (๐ โ if(๐ฅ โ ๐ด, ๐ต, 0) โ (0[,)+โ)) |
8 | 7 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, ๐ต, 0) โ (0[,)+โ)) |
9 | 8 | fmpttd 7064 |
. . . 4
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต,
0)):โโถ(0[,)+โ)) |
10 | | itgmulc2nc.3 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
11 | 1, 2 | iblpos 25160 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) โ โ))) |
12 | 10, 11 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) โ โ)) |
13 | 12 | simprd 497 |
. . . 4
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) โ โ) |
14 | | itgmulc2nc.4 |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
15 | | itgmulc2nc.6 |
. . . . 5
โข (๐ โ 0 โค ๐ถ) |
16 | | elrege0 13372 |
. . . . 5
โข (๐ถ โ (0[,)+โ) โ
(๐ถ โ โ โง 0
โค ๐ถ)) |
17 | 14, 15, 16 | sylanbrc 584 |
. . . 4
โข (๐ โ ๐ถ โ (0[,)+โ)) |
18 | 9, 13, 17 | itg2mulc 25115 |
. . 3
โข (๐ โ
(โซ2โ((โ ร {๐ถ}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) = (๐ถ ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))))) |
19 | | reex 11143 |
. . . . . . 7
โข โ
โ V |
20 | 19 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ
V) |
21 | | itgmulc2nc.1 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
22 | 21 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ ๐ถ โ โ) |
23 | | fconstmpt 5695 |
. . . . . . 7
โข (โ
ร {๐ถ}) = (๐ฅ โ โ โฆ ๐ถ) |
24 | 23 | a1i 11 |
. . . . . 6
โข (๐ โ (โ ร {๐ถ}) = (๐ฅ โ โ โฆ ๐ถ)) |
25 | | eqidd 2738 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
26 | 20, 22, 8, 24, 25 | offval2 7638 |
. . . . 5
โข (๐ โ ((โ ร {๐ถ}) โf ยท
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ฅ โ โ โฆ (๐ถ ยท if(๐ฅ โ ๐ด, ๐ต, 0)))) |
27 | | ovif2 7456 |
. . . . . . 7
โข (๐ถ ยท if(๐ฅ โ ๐ด, ๐ต, 0)) = if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), (๐ถ ยท 0)) |
28 | 21 | mul01d 11355 |
. . . . . . . . 9
โข (๐ โ (๐ถ ยท 0) = 0) |
29 | 28 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐ถ ยท 0) = 0) |
30 | 29 | ifeq2d 4507 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), (๐ถ ยท 0)) = if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0)) |
31 | 27, 30 | eqtrid 2789 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ (๐ถ ยท if(๐ฅ โ ๐ด, ๐ต, 0)) = if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0)) |
32 | 31 | mpteq2dva 5206 |
. . . . 5
โข (๐ โ (๐ฅ โ โ โฆ (๐ถ ยท if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0))) |
33 | 26, 32 | eqtrd 2777 |
. . . 4
โข (๐ โ ((โ ร {๐ถ}) โf ยท
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0))) |
34 | 33 | fveq2d 6847 |
. . 3
โข (๐ โ
(โซ2โ((โ ร {๐ถ}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0)))) |
35 | 18, 34 | eqtr3d 2779 |
. 2
โข (๐ โ (๐ถ ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0)))) |
36 | 1, 10, 2 | itgposval 25163 |
. . 3
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
37 | 36 | oveq2d 7374 |
. 2
โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = (๐ถ ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))))) |
38 | 14 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
39 | 38, 1 | remulcld 11186 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
40 | | itgmulc2nc.2 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
41 | | itgmulc2nc.m |
. . . 4
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ MblFn) |
42 | 21, 40, 10, 41 | iblmulc2nc 36146 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ
๐ฟ1) |
43 | 15 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ถ) |
44 | 38, 1, 43, 2 | mulge0d 11733 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (๐ถ ยท ๐ต)) |
45 | 39, 42, 44 | itgposval 25163 |
. 2
โข (๐ โ โซ๐ด(๐ถ ยท ๐ต) d๐ฅ = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (๐ถ ยท ๐ต), 0)))) |
46 | 35, 37, 45 | 3eqtr4d 2787 |
1
โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) |