Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
โข ((๐ฆ = (โโ๐ต) โง ๐ฅ โ ๐ด) โ ๐ฆ = (โโ๐ต)) |
2 | 1 | itgeq2dv 25169 |
. . . . . 6
โข (๐ฆ = (โโ๐ต) โ โซ๐ด๐ฆ d๐ฅ = โซ๐ด(โโ๐ต) d๐ฅ) |
3 | | oveq1 7368 |
. . . . . 6
โข (๐ฆ = (โโ๐ต) โ (๐ฆ ยท (volโ๐ด)) = ((โโ๐ต) ยท (volโ๐ด))) |
4 | 2, 3 | eqeq12d 2749 |
. . . . 5
โข (๐ฆ = (โโ๐ต) โ (โซ๐ด๐ฆ d๐ฅ = (๐ฆ ยท (volโ๐ด)) โ โซ๐ด(โโ๐ต) d๐ฅ = ((โโ๐ต) ยท (volโ๐ด)))) |
5 | | simplr 768 |
. . . . . . . 8
โข ((((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โง ๐ฅ โ
๐ด) โ ๐ฆ โ
โ) |
6 | | fconstmpt 5698 |
. . . . . . . . 9
โข (๐ด ร {๐ฆ}) = (๐ฅ โ ๐ด โฆ ๐ฆ) |
7 | | simpl1 1192 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ๐ด โ
dom vol) |
8 | | simp2 1138 |
. . . . . . . . . . 11
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (volโ๐ด) โ โ) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (volโ๐ด) โ โ) |
10 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ๐ฆ โ
โ) |
11 | 10 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ๐ฆ โ
โ) |
12 | | iblconst 25205 |
. . . . . . . . . 10
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ฆ โ
โ) โ (๐ด ร
{๐ฆ}) โ
๐ฟ1) |
13 | 7, 9, 11, 12 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (๐ด ร
{๐ฆ}) โ
๐ฟ1) |
14 | 6, 13 | eqeltrrid 2839 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (๐ฅ โ
๐ด โฆ ๐ฆ) โ
๐ฟ1) |
15 | 5, 14 | itgrevallem1 25182 |
. . . . . . 7
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ โซ๐ด๐ฆ d๐ฅ = ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0))))) |
16 | | ifan 4543 |
. . . . . . . . . . . 12
โข if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0) = if(๐ฅ โ ๐ด, if(0 โค ๐ฆ, ๐ฆ, 0), 0) |
17 | 16 | mpteq2i 5214 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค ๐ฆ, ๐ฆ, 0), 0)) |
18 | 17 | fveq2i 6849 |
. . . . . . . . . 10
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค ๐ฆ, ๐ฆ, 0), 0))) |
19 | | 0re 11165 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
20 | | ifcl 4535 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง 0 โ
โ) โ if(0 โค ๐ฆ, ๐ฆ, 0) โ โ) |
21 | 10, 19, 20 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค ๐ฆ, ๐ฆ, 0) โ โ) |
22 | | max1 13113 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง ๐ฆ
โ โ) โ 0 โค if(0 โค ๐ฆ, ๐ฆ, 0)) |
23 | 19, 10, 22 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ 0 โค if(0 โค ๐ฆ, ๐ฆ, 0)) |
24 | | elrege0 13380 |
. . . . . . . . . . . 12
โข (if(0
โค ๐ฆ, ๐ฆ, 0) โ (0[,)+โ) โ (if(0 โค
๐ฆ, ๐ฆ, 0) โ โ โง 0 โค if(0 โค
๐ฆ, ๐ฆ, 0))) |
25 | 21, 23, 24 | sylanbrc 584 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค ๐ฆ, ๐ฆ, 0) โ (0[,)+โ)) |
26 | | itg2const 25128 |
. . . . . . . . . . 11
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง if(0 โค ๐ฆ,
๐ฆ, 0) โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค ๐ฆ, ๐ฆ, 0), 0))) = (if(0 โค ๐ฆ, ๐ฆ, 0) ยท (volโ๐ด))) |
27 | 7, 9, 25, 26 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค ๐ฆ, ๐ฆ, 0), 0))) = (if(0 โค ๐ฆ, ๐ฆ, 0) ยท (volโ๐ด))) |
28 | 18, 27 | eqtrid 2785 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) = (if(0 โค ๐ฆ, ๐ฆ, 0) ยท (volโ๐ด))) |
29 | | ifan 4543 |
. . . . . . . . . . . 12
โข if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0) = if(๐ฅ โ ๐ด, if(0 โค -๐ฆ, -๐ฆ, 0), 0) |
30 | 29 | mpteq2i 5214 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค -๐ฆ, -๐ฆ, 0), 0)) |
31 | 30 | fveq2i 6849 |
. . . . . . . . . 10
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค -๐ฆ, -๐ฆ, 0), 0))) |
32 | | renegcl 11472 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ -๐ฆ โ
โ) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ -๐ฆ โ
โ) |
34 | | ifcl 4535 |
. . . . . . . . . . . . 13
โข ((-๐ฆ โ โ โง 0 โ
โ) โ if(0 โค -๐ฆ, -๐ฆ, 0) โ โ) |
35 | 33, 19, 34 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค -๐ฆ, -๐ฆ, 0) โ โ) |
36 | | max1 13113 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง -๐ฆ
โ โ) โ 0 โค if(0 โค -๐ฆ, -๐ฆ, 0)) |
37 | 19, 33, 36 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ 0 โค if(0 โค -๐ฆ, -๐ฆ, 0)) |
38 | | elrege0 13380 |
. . . . . . . . . . . 12
โข (if(0
โค -๐ฆ, -๐ฆ, 0) โ (0[,)+โ)
โ (if(0 โค -๐ฆ,
-๐ฆ, 0) โ โ โง
0 โค if(0 โค -๐ฆ, -๐ฆ, 0))) |
39 | 35, 37, 38 | sylanbrc 584 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค -๐ฆ, -๐ฆ, 0) โ (0[,)+โ)) |
40 | | itg2const 25128 |
. . . . . . . . . . 11
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง if(0 โค -๐ฆ,
-๐ฆ, 0) โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค -๐ฆ, -๐ฆ, 0), 0))) = (if(0 โค -๐ฆ, -๐ฆ, 0) ยท (volโ๐ด))) |
41 | 7, 9, 39, 40 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค -๐ฆ, -๐ฆ, 0), 0))) = (if(0 โค -๐ฆ, -๐ฆ, 0) ยท (volโ๐ด))) |
42 | 31, 41 | eqtrid 2785 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0))) = (if(0 โค -๐ฆ, -๐ฆ, 0) ยท (volโ๐ด))) |
43 | 28, 42 | oveq12d 7379 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0)))) = ((if(0 โค ๐ฆ, ๐ฆ, 0) ยท (volโ๐ด)) โ (if(0 โค -๐ฆ, -๐ฆ, 0) ยท (volโ๐ด)))) |
44 | 21 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค ๐ฆ, ๐ฆ, 0) โ โ) |
45 | 35 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ if(0 โค -๐ฆ, -๐ฆ, 0) โ โ) |
46 | 8 | recnd 11191 |
. . . . . . . . . 10
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (volโ๐ด) โ โ) |
47 | 46 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (volโ๐ด) โ โ) |
48 | 44, 45, 47 | subdird 11620 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ((if(0 โค ๐ฆ, ๐ฆ, 0) โ if(0 โค -๐ฆ, -๐ฆ, 0)) ยท (volโ๐ด)) = ((if(0 โค ๐ฆ, ๐ฆ, 0) ยท (volโ๐ด)) โ (if(0 โค -๐ฆ, -๐ฆ, 0) ยท (volโ๐ด)))) |
49 | | max0sub 13124 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (if(0
โค ๐ฆ, ๐ฆ, 0) โ if(0 โค -๐ฆ, -๐ฆ, 0)) = ๐ฆ) |
50 | 49 | adantl 483 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (if(0 โค ๐ฆ, ๐ฆ, 0) โ if(0 โค -๐ฆ, -๐ฆ, 0)) = ๐ฆ) |
51 | 50 | oveq1d 7376 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ ((if(0 โค ๐ฆ, ๐ฆ, 0) โ if(0 โค -๐ฆ, -๐ฆ, 0)) ยท (volโ๐ด)) = (๐ฆ ยท (volโ๐ด))) |
52 | 43, 48, 51 | 3eqtr2rd 2780 |
. . . . . . 7
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ (๐ฆ ยท
(volโ๐ด)) =
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ฆ), -๐ฆ, 0))))) |
53 | 15, 52 | eqtr4d 2776 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฆ โ
โ) โ โซ๐ด๐ฆ d๐ฅ = (๐ฆ ยท (volโ๐ด))) |
54 | 53 | ralrimiva 3140 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ โ๐ฆ
โ โ โซ๐ด๐ฆ d๐ฅ = (๐ฆ ยท (volโ๐ด))) |
55 | | recl 15004 |
. . . . . 6
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
56 | 55 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โโ๐ต) โ โ) |
57 | 4, 54, 56 | rspcdva 3584 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ โซ๐ด(โโ๐ต) d๐ฅ = ((โโ๐ต) ยท (volโ๐ด))) |
58 | | simpl 484 |
. . . . . . . . 9
โข ((๐ฆ = (โโ๐ต) โง ๐ฅ โ ๐ด) โ ๐ฆ = (โโ๐ต)) |
59 | 58 | itgeq2dv 25169 |
. . . . . . . 8
โข (๐ฆ = (โโ๐ต) โ โซ๐ด๐ฆ d๐ฅ = โซ๐ด(โโ๐ต) d๐ฅ) |
60 | | oveq1 7368 |
. . . . . . . 8
โข (๐ฆ = (โโ๐ต) โ (๐ฆ ยท (volโ๐ด)) = ((โโ๐ต) ยท (volโ๐ด))) |
61 | 59, 60 | eqeq12d 2749 |
. . . . . . 7
โข (๐ฆ = (โโ๐ต) โ (โซ๐ด๐ฆ d๐ฅ = (๐ฆ ยท (volโ๐ด)) โ โซ๐ด(โโ๐ต) d๐ฅ = ((โโ๐ต) ยท (volโ๐ด)))) |
62 | | imcl 15005 |
. . . . . . . 8
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
63 | 62 | 3ad2ant3 1136 |
. . . . . . 7
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โโ๐ต) โ โ) |
64 | 61, 54, 63 | rspcdva 3584 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ โซ๐ด(โโ๐ต) d๐ฅ = ((โโ๐ต) ยท (volโ๐ด))) |
65 | 64 | oveq2d 7377 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท ((โโ๐ต) ยท (volโ๐ด)))) |
66 | | ax-icn 11118 |
. . . . . . 7
โข i โ
โ |
67 | 66 | a1i 11 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ i โ โ) |
68 | 63 | recnd 11191 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โโ๐ต) โ โ) |
69 | 67, 68, 46 | mulassd 11186 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ ((i ยท (โโ๐ต)) ยท (volโ๐ด)) = (i ยท ((โโ๐ต) ยท (volโ๐ด)))) |
70 | 65, 69 | eqtr4d 2776 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) = ((i ยท (โโ๐ต)) ยท (volโ๐ด))) |
71 | 57, 70 | oveq12d 7379 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (((โโ๐ต) ยท (volโ๐ด)) + ((i ยท (โโ๐ต)) ยท (volโ๐ด)))) |
72 | 56 | recnd 11191 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โโ๐ต) โ โ) |
73 | | mulcl 11143 |
. . . . 5
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (i ยท
(โโ๐ต)) โ
โ) |
74 | 66, 68, 73 | sylancr 588 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (i ยท (โโ๐ต)) โ โ) |
75 | 72, 74, 46 | adddird 11188 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (((โโ๐ต) + (i ยท (โโ๐ต))) ยท (volโ๐ด)) = (((โโ๐ต) ยท (volโ๐ด)) + ((i ยท
(โโ๐ต)) ยท
(volโ๐ด)))) |
76 | 71, 75 | eqtr4d 2776 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (((โโ๐ต) + (i ยท (โโ๐ต))) ยท (volโ๐ด))) |
77 | | simpl3 1194 |
. . 3
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โง ๐ฅ โ
๐ด) โ ๐ต โ โ) |
78 | | fconstmpt 5698 |
. . . 4
โข (๐ด ร {๐ต}) = (๐ฅ โ ๐ด โฆ ๐ต) |
79 | | iblconst 25205 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (๐ด ร
{๐ต}) โ
๐ฟ1) |
80 | 78, 79 | eqeltrrid 2839 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (๐ฅ โ
๐ด โฆ ๐ต) โ
๐ฟ1) |
81 | 77, 80 | itgcnval 25187 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
82 | | replim 15010 |
. . . 4
โข (๐ต โ โ โ ๐ต = ((โโ๐ต) + (i ยท
(โโ๐ต)))) |
83 | 82 | 3ad2ant3 1136 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ ๐ต =
((โโ๐ต) + (i
ยท (โโ๐ต)))) |
84 | 83 | oveq1d 7376 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ (๐ต ยท
(volโ๐ด)) =
(((โโ๐ต) + (i
ยท (โโ๐ต))) ยท (volโ๐ด))) |
85 | 76, 81, 84 | 3eqtr4d 2783 |
1
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
โ) โ โซ๐ด๐ต d๐ฅ = (๐ต ยท (volโ๐ด))) |