Step | Hyp | Ref
| Expression |
1 | | ovol0 24873 |
. . . . 5
โข
(vol*โโ
) = 0 |
2 | | 0mbl 24919 |
. . . . . 6
โข โ
โ dom vol |
3 | | mblvol 24910 |
. . . . . 6
โข (โ
โ dom vol โ (volโโ
) =
(vol*โโ
)) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
โข
(volโโ
) = (vol*โโ
) |
5 | | itg10 25068 |
. . . . 5
โข
(โซ1โ(โ ร {0})) = 0 |
6 | 1, 4, 5 | 3eqtr4ri 2776 |
. . . 4
โข
(โซ1โ(โ ร {0})) =
(volโโ
) |
7 | | noel 4295 |
. . . . . . . . 9
โข ยฌ
๐ฅ โ
โ
|
8 | | eleq2 2827 |
. . . . . . . . 9
โข (๐ด = โ
โ (๐ฅ โ ๐ด โ ๐ฅ โ โ
)) |
9 | 7, 8 | mtbiri 327 |
. . . . . . . 8
โข (๐ด = โ
โ ยฌ ๐ฅ โ ๐ด) |
10 | 9 | iffalsed 4502 |
. . . . . . 7
โข (๐ด = โ
โ if(๐ฅ โ ๐ด, 1, 0) = 0) |
11 | 10 | mpteq2dv 5212 |
. . . . . 6
โข (๐ด = โ
โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0)) = (๐ฅ โ โ โฆ 0)) |
12 | | i1f1.1 |
. . . . . 6
โข ๐น = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, 1, 0)) |
13 | | fconstmpt 5699 |
. . . . . 6
โข (โ
ร {0}) = (๐ฅ โ
โ โฆ 0) |
14 | 11, 12, 13 | 3eqtr4g 2802 |
. . . . 5
โข (๐ด = โ
โ ๐น = (โ ร
{0})) |
15 | 14 | fveq2d 6851 |
. . . 4
โข (๐ด = โ
โ
(โซ1โ๐น)
= (โซ1โ(โ ร {0}))) |
16 | | fveq2 6847 |
. . . 4
โข (๐ด = โ
โ
(volโ๐ด) =
(volโโ
)) |
17 | 6, 15, 16 | 3eqtr4a 2803 |
. . 3
โข (๐ด = โ
โ
(โซ1โ๐น)
= (volโ๐ด)) |
18 | 17 | a1i 11 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (๐ด =
โ
โ (โซ1โ๐น) = (volโ๐ด))) |
19 | | n0 4311 |
. . 3
โข (๐ด โ โ
โ
โ๐ฆ ๐ฆ โ ๐ด) |
20 | 12 | i1f1 25070 |
. . . . . . . 8
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ ๐น โ
dom โซ1) |
21 | 20 | adantr 482 |
. . . . . . 7
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ๐น โ dom
โซ1) |
22 | | itg1val 25063 |
. . . . . . 7
โข (๐น โ dom โซ1
โ (โซ1โ๐น) = ฮฃ๐ง โ (ran ๐น โ {0})(๐ง ยท (volโ(โก๐น โ {๐ง})))) |
23 | 21, 22 | syl 17 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ
(โซ1โ๐น)
= ฮฃ๐ง โ (ran
๐น โ {0})(๐ง ยท (volโ(โก๐น โ {๐ง})))) |
24 | 12 | i1f1lem 25069 |
. . . . . . . . . . . . . 14
โข (๐น:โโถ{0, 1} โง
(๐ด โ dom vol โ
(โก๐น โ {1}) = ๐ด)) |
25 | 24 | simpli 485 |
. . . . . . . . . . . . 13
โข ๐น:โโถ{0,
1} |
26 | | frn 6680 |
. . . . . . . . . . . . 13
โข (๐น:โโถ{0, 1} โ
ran ๐น โ {0,
1}) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
โข ran ๐น โ {0, 1} |
28 | | ssdif 4104 |
. . . . . . . . . . . 12
โข (ran
๐น โ {0, 1} โ
(ran ๐น โ {0}) โ
({0, 1} โ {0})) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
โข (ran
๐น โ {0}) โ ({0,
1} โ {0}) |
30 | | difprsnss 4764 |
. . . . . . . . . . 11
โข ({0, 1}
โ {0}) โ {1} |
31 | 29, 30 | sstri 3958 |
. . . . . . . . . 10
โข (ran
๐น โ {0}) โ
{1} |
32 | 31 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (ran ๐น โ {0}) โ
{1}) |
33 | | mblss 24911 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ dom vol โ ๐ด โ
โ) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ ๐ด โ
โ) |
35 | 34 | sselda 3949 |
. . . . . . . . . . . . . 14
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ๐ฆ โ
โ) |
36 | | eleq1w 2821 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ฆ โ (๐ฅ โ ๐ด โ ๐ฆ โ ๐ด)) |
37 | 36 | ifbid 4514 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ฆ โ if(๐ฅ โ ๐ด, 1, 0) = if(๐ฆ โ ๐ด, 1, 0)) |
38 | | 1ex 11158 |
. . . . . . . . . . . . . . . 16
โข 1 โ
V |
39 | | c0ex 11156 |
. . . . . . . . . . . . . . . 16
โข 0 โ
V |
40 | 38, 39 | ifex 4541 |
. . . . . . . . . . . . . . 15
โข if(๐ฆ โ ๐ด, 1, 0) โ V |
41 | 37, 12, 40 | fvmpt 6953 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐นโ๐ฆ) = if(๐ฆ โ ๐ด, 1, 0)) |
42 | 35, 41 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (๐นโ๐ฆ) = if(๐ฆ โ ๐ด, 1, 0)) |
43 | | iftrue 4497 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ ๐ด โ if(๐ฆ โ ๐ด, 1, 0) = 1) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ if(๐ฆ โ ๐ด, 1, 0) = 1) |
45 | 42, 44 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (๐นโ๐ฆ) = 1) |
46 | | ffn 6673 |
. . . . . . . . . . . . . 14
โข (๐น:โโถ{0, 1} โ
๐น Fn
โ) |
47 | 25, 46 | ax-mp 5 |
. . . . . . . . . . . . 13
โข ๐น Fn โ |
48 | | fnfvelrn 7036 |
. . . . . . . . . . . . 13
โข ((๐น Fn โ โง ๐ฆ โ โ) โ (๐นโ๐ฆ) โ ran ๐น) |
49 | 47, 35, 48 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (๐นโ๐ฆ) โ ran ๐น) |
50 | 45, 49 | eqeltrrd 2839 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ 1 โ ran
๐น) |
51 | | ax-1ne0 11127 |
. . . . . . . . . . 11
โข 1 โ
0 |
52 | | eldifsn 4752 |
. . . . . . . . . . 11
โข (1 โ
(ran ๐น โ {0}) โ
(1 โ ran ๐น โง 1
โ 0)) |
53 | 50, 51, 52 | sylanblrc 591 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ 1 โ (ran
๐น โ
{0})) |
54 | 53 | snssd 4774 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ {1} โ (ran
๐น โ
{0})) |
55 | 32, 54 | eqssd 3966 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (ran ๐น โ {0}) =
{1}) |
56 | 55 | sumeq1d 15593 |
. . . . . . 7
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ฮฃ๐ง โ (ran ๐น โ {0})(๐ง ยท (volโ(โก๐น โ {๐ง}))) = ฮฃ๐ง โ {1} (๐ง ยท (volโ(โก๐น โ {๐ง})))) |
57 | | 1re 11162 |
. . . . . . . . 9
โข 1 โ
โ |
58 | 24 | simpri 487 |
. . . . . . . . . . . . . 14
โข (๐ด โ dom vol โ (โก๐น โ {1}) = ๐ด) |
59 | 58 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (โก๐น โ {1}) = ๐ด) |
60 | 59 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (volโ(โก๐น โ {1})) = (volโ๐ด)) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (1 ยท
(volโ(โก๐น โ {1}))) = (1 ยท
(volโ๐ด))) |
62 | | simplr 768 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (volโ๐ด) โ
โ) |
63 | 62 | recnd 11190 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (volโ๐ด) โ
โ) |
64 | 63 | mulid2d 11180 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (1 ยท
(volโ๐ด)) =
(volโ๐ด)) |
65 | 61, 64 | eqtrd 2777 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (1 ยท
(volโ(โก๐น โ {1}))) = (volโ๐ด)) |
66 | 65, 63 | eqeltrd 2838 |
. . . . . . . . 9
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ (1 ยท
(volโ(โก๐น โ {1}))) โ
โ) |
67 | | id 22 |
. . . . . . . . . . 11
โข (๐ง = 1 โ ๐ง = 1) |
68 | | sneq 4601 |
. . . . . . . . . . . . 13
โข (๐ง = 1 โ {๐ง} = {1}) |
69 | 68 | imaeq2d 6018 |
. . . . . . . . . . . 12
โข (๐ง = 1 โ (โก๐น โ {๐ง}) = (โก๐น โ {1})) |
70 | 69 | fveq2d 6851 |
. . . . . . . . . . 11
โข (๐ง = 1 โ (volโ(โก๐น โ {๐ง})) = (volโ(โก๐น โ {1}))) |
71 | 67, 70 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ง = 1 โ (๐ง ยท (volโ(โก๐น โ {๐ง}))) = (1 ยท (volโ(โก๐น โ {1})))) |
72 | 71 | sumsn 15638 |
. . . . . . . . 9
โข ((1
โ โ โง (1 ยท (volโ(โก๐น โ {1}))) โ โ) โ
ฮฃ๐ง โ {1} (๐ง ยท (volโ(โก๐น โ {๐ง}))) = (1 ยท (volโ(โก๐น โ {1})))) |
73 | 57, 66, 72 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ฮฃ๐ง โ {1} (๐ง ยท (volโ(โก๐น โ {๐ง}))) = (1 ยท (volโ(โก๐น โ {1})))) |
74 | 73, 65 | eqtrd 2777 |
. . . . . . 7
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ฮฃ๐ง โ {1} (๐ง ยท (volโ(โก๐น โ {๐ง}))) = (volโ๐ด)) |
75 | 56, 74 | eqtrd 2777 |
. . . . . 6
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ ฮฃ๐ง โ (ran ๐น โ {0})(๐ง ยท (volโ(โก๐น โ {๐ง}))) = (volโ๐ด)) |
76 | 23, 75 | eqtrd 2777 |
. . . . 5
โข (((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โง ๐ฆ โ
๐ด) โ
(โซ1โ๐น)
= (volโ๐ด)) |
77 | 76 | ex 414 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (๐ฆ โ
๐ด โ
(โซ1โ๐น)
= (volโ๐ด))) |
78 | 77 | exlimdv 1937 |
. . 3
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (โ๐ฆ
๐ฆ โ ๐ด โ (โซ1โ๐น) = (volโ๐ด))) |
79 | 19, 78 | biimtrid 241 |
. 2
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (๐ด โ
โ
โ (โซ1โ๐น) = (volโ๐ด))) |
80 | 18, 79 | pm2.61dne 3032 |
1
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ) โ (โซ1โ๐น) = (volโ๐ด)) |