Step | Hyp | Ref
| Expression |
1 | | reex 11200 |
. . . . . . 7
โข โ
โ V |
2 | 1 | a1i 11 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ โ โ V) |
3 | | simpl3 1193 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โง ๐ฅ
โ โ) โ ๐ต
โ (0[,)+โ)) |
4 | | 1re 11213 |
. . . . . . . 8
โข 1 โ
โ |
5 | | 0re 11215 |
. . . . . . . 8
โข 0 โ
โ |
6 | 4, 5 | ifcli 4575 |
. . . . . . 7
โข if(๐ฅ โ ๐ด, 1, 0) โ โ |
7 | 6 | a1i 11 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โง ๐ฅ
โ โ) โ if(๐ฅ
โ ๐ด, 1, 0) โ
โ) |
8 | | fconstmpt 5738 |
. . . . . . 7
โข (โ
ร {๐ต}) = (๐ฅ โ โ โฆ ๐ต) |
9 | 8 | a1i 11 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โ ร {๐ต}) = (๐ฅ โ โ โฆ ๐ต)) |
10 | | eqidd 2733 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, 1, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) |
11 | 2, 3, 7, 9, 10 | offval2 7689 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ((โ ร {๐ต}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) = (๐ฅ โ โ โฆ (๐ต ยท if(๐ฅ โ ๐ด, 1, 0)))) |
12 | | ovif2 7506 |
. . . . . . 7
โข (๐ต ยท if(๐ฅ โ ๐ด, 1, 0)) = if(๐ฅ โ ๐ด, (๐ต ยท 1), (๐ต ยท 0)) |
13 | | simp3 1138 |
. . . . . . . . . . . 12
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ๐ต
โ (0[,)+โ)) |
14 | | elrege0 13430 |
. . . . . . . . . . . 12
โข (๐ต โ (0[,)+โ) โ
(๐ต โ โ โง 0
โค ๐ต)) |
15 | 13, 14 | sylib 217 |
. . . . . . . . . . 11
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ต
โ โ โง 0 โค ๐ต)) |
16 | 15 | simpld 495 |
. . . . . . . . . 10
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ๐ต
โ โ) |
17 | 16 | recnd 11241 |
. . . . . . . . 9
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ๐ต
โ โ) |
18 | 17 | mulridd 11230 |
. . . . . . . 8
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ต
ยท 1) = ๐ต) |
19 | 17 | mul01d 11412 |
. . . . . . . 8
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ต
ยท 0) = 0) |
20 | 18, 19 | ifeq12d 4549 |
. . . . . . 7
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ if(๐ฅ
โ ๐ด, (๐ต ยท 1), (๐ต ยท 0)) = if(๐ฅ โ ๐ด, ๐ต, 0)) |
21 | 12, 20 | eqtrid 2784 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ต
ยท if(๐ฅ โ ๐ด, 1, 0)) = if(๐ฅ โ ๐ด, ๐ต, 0)) |
22 | 21 | mpteq2dv 5250 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ (๐ต
ยท if(๐ฅ โ ๐ด, 1, 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
23 | 11, 22 | eqtrd 2772 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ((โ ร {๐ต}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
24 | | eqid 2732 |
. . . . . . 7
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0)) |
25 | 24 | i1f1 25206 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (๐ฅ โ
โ โฆ if(๐ฅ โ
๐ด, 1, 0)) โ dom
โซ1) |
26 | 25 | 3adant3 1132 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, 1, 0)) โ dom
โซ1) |
27 | 26, 16 | i1fmulc 25220 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ((โ ร {๐ต}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) โ dom
โซ1) |
28 | 23, 27 | eqeltrrd 2834 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)) โ dom
โซ1) |
29 | 15 | simprd 496 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ 0 โค ๐ต) |
30 | | 0le0 12312 |
. . . . . 6
โข 0 โค
0 |
31 | | breq2 5152 |
. . . . . . 7
โข (๐ต = if(๐ฅ โ ๐ด, ๐ต, 0) โ (0 โค ๐ต โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
32 | | breq2 5152 |
. . . . . . 7
โข (0 =
if(๐ฅ โ ๐ด, ๐ต, 0) โ (0 โค 0 โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
33 | 31, 32 | ifboth 4567 |
. . . . . 6
โข ((0 โค
๐ต โง 0 โค 0) โ 0
โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
34 | 29, 30, 33 | sylancl 586 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
35 | 34 | ralrimivw 3150 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ โ๐ฅ โ โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
36 | | ax-resscn 11166 |
. . . . . . 7
โข โ
โ โ |
37 | 36 | a1i 11 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ โ โ โ) |
38 | 16 | adantr 481 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โง ๐ฅ
โ โ) โ ๐ต
โ โ) |
39 | | ifcl 4573 |
. . . . . . . . 9
โข ((๐ต โ โ โง 0 โ
โ) โ if(๐ฅ โ
๐ด, ๐ต, 0) โ โ) |
40 | 38, 5, 39 | sylancl 586 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โง ๐ฅ
โ โ) โ if(๐ฅ
โ ๐ด, ๐ต, 0) โ โ) |
41 | 40 | ralrimiva 3146 |
. . . . . . 7
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ โ๐ฅ โ โ if(๐ฅ โ ๐ด, ๐ต, 0) โ โ) |
42 | | eqid 2732 |
. . . . . . . 8
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) |
43 | 42 | fnmpt 6690 |
. . . . . . 7
โข
(โ๐ฅ โ
โ if(๐ฅ โ ๐ด, ๐ต, 0) โ โ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) Fn โ) |
44 | 41, 43 | syl 17 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)) Fn โ) |
45 | 37, 44 | 0pledm 25189 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (0๐ โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) โ (โ ร {0})
โr โค (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)))) |
46 | 5 | a1i 11 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โง ๐ฅ
โ โ) โ 0 โ โ) |
47 | | fconstmpt 5738 |
. . . . . . 7
โข (โ
ร {0}) = (๐ฅ โ
โ โฆ 0) |
48 | 47 | a1i 11 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โ ร {0}) = (๐ฅ โ โ โฆ 0)) |
49 | | eqidd 2733 |
. . . . . 6
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
50 | 2, 46, 40, 48, 49 | ofrfval2 7690 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ ((โ ร {0}) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) โ โ๐ฅ โ โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
51 | 45, 50 | bitrd 278 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (0๐ โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) โ โ๐ฅ โ โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
52 | 35, 51 | mpbird 256 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ 0๐ โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
53 | | itg2itg1 25253 |
. . 3
โข (((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) โ dom โซ1 โง
0๐ โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) = (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
54 | 28, 52, 53 | syl2anc 584 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) = (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
55 | 26, 16 | itg1mulc 25221 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ1โ((โ ร {๐ต}) โf ยท
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, 1, 0)))) = (๐ต ยท (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))))) |
56 | 23 | fveq2d 6895 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ1โ((โ ร {๐ต}) โf ยท
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, 1, 0)))) =
(โซ1โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)))) |
57 | 24 | itg11 25207 |
. . . . 5
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) = (volโ๐ด)) |
58 | 57 | 3adant3 1132 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0))) = (volโ๐ด)) |
59 | 58 | oveq2d 7424 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (๐ต
ยท (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0)))) = (๐ต ยท (volโ๐ด))) |
60 | 55, 56, 59 | 3eqtr3d 2780 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ1โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ต ยท (volโ๐ด))) |
61 | 54, 60 | eqtrd 2772 |
1
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ต ยท (volโ๐ด))) |