Step | Hyp | Ref
| Expression |
1 | | unieq 4877 |
. . . . . . . . 9
โข (๐ด = โ
โ โช ๐ด =
โช โ
) |
2 | | uni0 4897 |
. . . . . . . . 9
โข โช โ
= โ
|
3 | 1, 2 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ด = โ
โ โช ๐ด =
โ
) |
4 | 3 | fveq2d 6847 |
. . . . . . 7
โข (๐ด = โ
โ
(volโโช ๐ด) = (volโโ
)) |
5 | | 0mbl 24919 |
. . . . . . . . 9
โข โ
โ dom vol |
6 | | mblvol 24910 |
. . . . . . . . 9
โข (โ
โ dom vol โ (volโโ
) =
(vol*โโ
)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
โข
(volโโ
) = (vol*โโ
) |
8 | | ovol0 24873 |
. . . . . . . 8
โข
(vol*โโ
) = 0 |
9 | 7, 8 | eqtri 2761 |
. . . . . . 7
โข
(volโโ
) = 0 |
10 | 4, 9 | eqtr2di 2790 |
. . . . . 6
โข (๐ด = โ
โ 0 =
(volโโช ๐ด)) |
11 | 10 | a1d 25 |
. . . . 5
โข (๐ด = โ
โ ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (volโโช ๐ด))) |
12 | | reldom 8892 |
. . . . . . . . . . 11
โข Rel
โผ |
13 | 12 | brrelex1i 5689 |
. . . . . . . . . 10
โข (๐ด โผ โ โ ๐ด โ V) |
14 | | 0sdomg 9051 |
. . . . . . . . . 10
โข (๐ด โ V โ (โ
โบ ๐ด โ ๐ด โ โ
)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
โข (๐ด โผ โ โ (โ
โบ ๐ด โ ๐ด โ โ
)) |
16 | 15 | biimparc 481 |
. . . . . . . 8
โข ((๐ด โ โ
โง ๐ด โผ โ) โ โ
โบ ๐ด) |
17 | | fodomr 9075 |
. . . . . . . 8
โข ((โ
โบ ๐ด โง ๐ด โผ โ) โ
โ๐ ๐:โโontoโ๐ด) |
18 | 16, 17 | sylancom 589 |
. . . . . . 7
โข ((๐ด โ โ
โง ๐ด โผ โ) โ
โ๐ ๐:โโontoโ๐ด) |
19 | | unissb 4901 |
. . . . . . . . . . . . 13
โข (โช ๐ด
โ โ โ โ๐ฅ โ ๐ด ๐ฅ โ โ) |
20 | 19 | anbi1i 625 |
. . . . . . . . . . . 12
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ (โ๐ฅ โ ๐ด ๐ฅ โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ)) |
21 | | r19.26 3111 |
. . . . . . . . . . . 12
โข
(โ๐ฅ โ
๐ด (๐ฅ โ โ โง ๐ฅ โผ โ) โ (โ๐ฅ โ ๐ด ๐ฅ โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ)) |
22 | 20, 21 | bitr4i 278 |
. . . . . . . . . . 11
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง ๐ฅ โผ โ)) |
23 | | ovolctb2 24872 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฅ โผ โ) โ
(vol*โ๐ฅ) =
0) |
24 | 23 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ (๐ฅ โผ โ โ
(vol*โ๐ฅ) =
0)) |
25 | 24 | imdistani 570 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฅ โผ โ) โ (๐ฅ โ โ โง
(vol*โ๐ฅ) =
0)) |
26 | 25 | ralimi 3083 |
. . . . . . . . . . 11
โข
(โ๐ฅ โ
๐ด (๐ฅ โ โ โง ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
27 | 22, 26 | sylbi 216 |
. . . . . . . . . 10
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
28 | 27 | ancoms 460 |
. . . . . . . . 9
โข
((โ๐ฅ โ
๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
29 | | foima 6762 |
. . . . . . . . . . . 12
โข (๐:โโontoโ๐ด โ (๐ โ โ) = ๐ด) |
30 | 29 | raleqdv 3312 |
. . . . . . . . . . 11
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0))) |
31 | | fofn 6759 |
. . . . . . . . . . . 12
โข (๐:โโontoโ๐ด โ ๐ Fn โ) |
32 | | ssid 3967 |
. . . . . . . . . . . 12
โข โ
โ โ |
33 | | sseq1 3970 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐โ๐) โ (๐ฅ โ โ โ (๐โ๐) โ โ)) |
34 | | fveqeq2 6852 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐โ๐) โ ((vol*โ๐ฅ) = 0 โ (vol*โ(๐โ๐)) = 0)) |
35 | 33, 34 | anbi12d 632 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐โ๐) โ ((๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
36 | 35 | ralima 7189 |
. . . . . . . . . . . 12
โข ((๐ Fn โ โง โ
โ โ) โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
37 | 31, 32, 36 | sylancl 587 |
. . . . . . . . . . 11
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
38 | 30, 37 | bitr3d 281 |
. . . . . . . . . 10
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
39 | | difss 4092 |
. . . . . . . . . . . . . . . . . 18
โข ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ (๐โ๐) |
40 | | ovolssnul 24867 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ (๐โ๐) โง (๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
41 | 39, 40 | mp3an1 1449 |
. . . . . . . . . . . . . . . . 17
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
42 | | ssdifss 4096 |
. . . . . . . . . . . . . . . . . 18
โข ((๐โ๐) โ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ) |
43 | | nulmbl 24915 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol) |
44 | | mblvol 24910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
45 | 44 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ ((volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0 โ (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0)) |
46 | 45 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
47 | | 0re 11162 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 โ
โ |
48 | 46, 47 | eqeltrdi 2842 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ) |
49 | 48 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0 โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
50 | 49 | ancld 552 |
. . . . . . . . . . . . . . . . . . . 20
โข
((vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0 โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ))) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ))) |
52 | 43, 51 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
53 | 42, 52 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข (((๐โ๐) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
54 | 41, 53 | syldan 592 |
. . . . . . . . . . . . . . . 16
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
55 | 54 | ralimi 3083 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ โ๐ โ โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
56 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
57 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ (1..^๐) = (1..^๐)) |
58 | 57 | iuneq1d 4982 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ โช
๐ โ (1..^๐)(๐โ๐) = โช ๐ โ (1..^๐)(๐โ๐)) |
59 | 56, 58 | difeq12d 4084 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) = ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
60 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
61 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐โ๐) โ V |
62 | | difexg 5285 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ๐) โ V โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ V) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ V |
64 | 59, 60, 63 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) = ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
65 | 64 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol)) |
66 | 64 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ
(volโ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) = (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
67 | 66 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((volโ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
68 | 65, 67 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ))) |
69 | 68 | ralbiia 3091 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ (((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โ โ๐ โ โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
70 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
71 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (1..^๐) = (1..^๐)) |
72 | 71 | iuneq1d 4982 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ โช
๐ โ (1..^๐)(๐โ๐) = โช ๐ โ (1..^๐)(๐โ๐)) |
73 | 70, 72 | difeq12d 4084 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) = ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
74 | 73 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol)) |
75 | 73 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
76 | 75 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ ((volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
77 | 74, 76 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ))) |
78 | 77 | cbvralvw 3224 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ (((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ) โ โ๐ โ โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
79 | 69, 78 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ (((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โ โ๐ โ โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โง (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โ)) |
80 | 55, 79 | sylibr 233 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ โ๐ โ โ (((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ)) |
81 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
82 | 81 | iundisj2 24929 |
. . . . . . . . . . . . . . 15
โข
Disj ๐ โ
โ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)) |
83 | | disjeq2 5075 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ ((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) = ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ (Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ Disj ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
84 | 83, 64 | mprg 3067 |
. . . . . . . . . . . . . . 15
โข
(Disj ๐
โ โ ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ Disj ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
85 | 82, 84 | mpbir 230 |
. . . . . . . . . . . . . 14
โข
Disj ๐ โ
โ ((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) |
86 | | nnex 12164 |
. . . . . . . . . . . . . . . . 17
โข โ
โ V |
87 | 86 | mptex 7174 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ V |
88 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (๐โ๐) = ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) |
89 | 88 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ ((๐โ๐) โ dom vol โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol)) |
90 | 88 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (volโ(๐โ๐)) = (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))) |
91 | 90 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ ((volโ(๐โ๐)) โ โ โ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ)) |
92 | 89, 91 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (((๐โ๐) โ dom vol โง (volโ(๐โ๐)) โ โ) โ (((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ))) |
93 | 92 | ralbidv 3171 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (โ๐ โ โ ((๐โ๐) โ dom vol โง (volโ(๐โ๐)) โ โ) โ โ๐ โ โ (((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ))) |
94 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โง ๐ โ โ) โ (๐โ๐) = ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) |
95 | 94 | disjeq2dv 5076 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (Disj ๐ โ โ (๐โ๐) โ Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))) |
96 | 93, 95 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ ((โ๐ โ โ ((๐โ๐) โ dom vol โง (volโ(๐โ๐)) โ โ) โง Disj ๐ โ โ (๐โ๐)) โ (โ๐ โ โ (((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โง Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))) |
97 | 88 | iuneq2d 4984 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ โช ๐ โ โ (๐โ๐) = โช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) |
98 | 97 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (volโโช ๐ โ โ (๐โ๐)) = (volโโช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))) |
99 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ = seq1( + , ๐บ) |
100 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐บ = (๐ โ โ โฆ (volโ(๐โ๐))) |
101 | | seqeq3 13917 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐บ = (๐ โ โ โฆ (volโ(๐โ๐))) โ seq1( + , ๐บ) = seq1( + , (๐ โ โ โฆ (volโ(๐โ๐))))) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
โข seq1( + ,
๐บ) = seq1( + , (๐ โ โ โฆ
(volโ(๐โ๐)))) |
103 | 99, 102 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ = seq1( + , (๐ โ โ โฆ (volโ(๐โ๐)))) |
104 | 103 | rneqi 5893 |
. . . . . . . . . . . . . . . . . . . 20
โข ran ๐ = ran seq1( + , (๐ โ โ โฆ
(volโ(๐โ๐)))) |
105 | 104 | supeq1i 9388 |
. . . . . . . . . . . . . . . . . . 19
โข sup(ran
๐, โ*,
< ) = sup(ran seq1( + , (๐ โ โ โฆ (volโ(๐โ๐)))), โ*, <
) |
106 | 90 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (๐ โ โ โฆ (volโ(๐โ๐))) = (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))) |
107 | 106 | seqeq3d 13920 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ seq1( + , (๐ โ โ โฆ (volโ(๐โ๐)))) = seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))))) |
108 | 107 | rneqd 5894 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ ran seq1( + , (๐ โ โ โฆ (volโ(๐โ๐)))) = ran seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))))) |
109 | 108 | supeq1d 9387 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ sup(ran seq1( + , (๐ โ โ โฆ
(volโ(๐โ๐)))), โ*, <
) = sup(ran seq1( + , (๐
โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, <
)) |
110 | 105, 109 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ sup(ran ๐, โ*, < ) = sup(ran
seq1( + , (๐ โ โ
โฆ (volโ((๐
โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, <
)) |
111 | 98, 110 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ ((volโโช ๐ โ โ (๐โ๐)) = sup(ran ๐, โ*, < ) โ
(volโโช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, <
))) |
112 | 96, 111 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) โ (((โ๐ โ โ ((๐โ๐) โ dom vol โง (volโ(๐โ๐)) โ โ) โง Disj ๐ โ โ (๐โ๐)) โ (volโโช ๐ โ โ (๐โ๐)) = sup(ran ๐, โ*, < )) โ
((โ๐ โ โ
(((๐ โ โ โฆ
((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โง Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ (volโโช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, <
)))) |
113 | | voliunnfl.3 |
. . . . . . . . . . . . . . . 16
โข
((โ๐ โ
โ ((๐โ๐) โ dom vol โง
(volโ(๐โ๐)) โ โ) โง
Disj ๐ โ
โ (๐โ๐)) โ (volโโช ๐ โ โ (๐โ๐)) = sup(ran ๐, โ*, <
)) |
114 | 87, 112, 113 | vtocl 3517 |
. . . . . . . . . . . . . . 15
โข
((โ๐ โ
โ (((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โง Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ (volโโช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, <
)) |
115 | 64 | iuneq2i 4976 |
. . . . . . . . . . . . . . . 16
โข โช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐) = โช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) |
116 | 115 | fveq2i 6846 |
. . . . . . . . . . . . . . 15
โข
(volโโช ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) = (volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) |
117 | 66 | mpteq2ia 5209 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โฆ
(volโ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))) = (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
118 | | seqeq3 13917 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โฆ
(volโ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐))) = (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) โ seq1( + , (๐ โ โ โฆ (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))) = seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))))) |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข seq1( + ,
(๐ โ โ โฆ
(volโ((๐ โ
โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))) = seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))) |
120 | 119 | rneqi 5893 |
. . . . . . . . . . . . . . . 16
โข ran seq1(
+ , (๐ โ โ
โฆ (volโ((๐
โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))) = ran seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))) |
121 | 120 | supeq1i 9388 |
. . . . . . . . . . . . . . 15
โข sup(ran
seq1( + , (๐ โ โ
โฆ (volโ((๐
โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)))), โ*, < ) = sup(ran
seq1( + , (๐ โ โ
โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))), โ*, <
) |
122 | 114, 116,
121 | 3eqtr3g 2796 |
. . . . . . . . . . . . . 14
โข
((โ๐ โ
โ (((๐ โ โ
โฆ ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))โ๐) โ dom vol โง (volโ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ โ) โง Disj ๐ โ โ ((๐ โ โ โฆ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))โ๐)) โ (volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))), โ*, <
)) |
123 | 80, 85, 122 | sylancl 587 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ
(volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))), โ*, <
)) |
124 | 123 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ (volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = sup(ran seq1( + , (๐ โ โ โฆ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))))), โ*, <
)) |
125 | 81 | iundisj 24928 |
. . . . . . . . . . . . . . . 16
โข โช ๐ โ โ (๐โ๐) = โช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) |
126 | | fofun 6758 |
. . . . . . . . . . . . . . . . 17
โข (๐:โโontoโ๐ด โ Fun ๐) |
127 | | funiunfv 7196 |
. . . . . . . . . . . . . . . . 17
โข (Fun
๐ โ โช ๐ โ โ (๐โ๐) = โช (๐ โ
โ)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐:โโontoโ๐ด โ โช
๐ โ โ (๐โ๐) = โช (๐ โ
โ)) |
129 | 125, 128 | eqtr3id 2787 |
. . . . . . . . . . . . . . 15
โข (๐:โโontoโ๐ด โ โช
๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) = โช (๐ โ
โ)) |
130 | 29 | unieqd 4880 |
. . . . . . . . . . . . . . 15
โข (๐:โโontoโ๐ด โ โช (๐ โ โ) = โช ๐ด) |
131 | 129, 130 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐:โโontoโ๐ด โ โช
๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) = โช ๐ด) |
132 | 131 | fveq2d 6847 |
. . . . . . . . . . . . 13
โข (๐:โโontoโ๐ด โ (volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (volโโช
๐ด)) |
133 | 132 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ (volโโช ๐ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (volโโช
๐ด)) |
134 | 56 | sseq1d 3976 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ ((๐โ๐) โ โ โ (๐โ๐) โ โ)) |
135 | 56 | fveqeq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ ((vol*โ(๐โ๐)) = 0 โ (vol*โ(๐โ๐)) = 0)) |
136 | 134, 135 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
137 | 136 | rspccva 3579 |
. . . . . . . . . . . . . . . . . . 19
โข
((โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โง ๐ โ โ) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) |
138 | | ssdifss 4096 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ๐) โ โ โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ) |
140 | | difss 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ (๐โ๐) |
141 | | ovolssnul 24867 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ (๐โ๐) โง (๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
142 | 140, 141 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
143 | 139, 142 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0)) |
144 | | nulmbl 24915 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ โ โง (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) โ ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol) |
145 | | mblvol 24910 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)) โ dom vol โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
146 | 143, 144,
145 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = (vol*โ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐)))) |
147 | 146, 142 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
148 | 137, 147 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข
((โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โง ๐ โ โ) โ (volโ((๐โ๐) โ โช
๐ โ (1..^๐)(๐โ๐))) = 0) |
149 | 148 | mpteq2dva 5206 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ (๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐)))) = (๐ โ โ โฆ 0)) |
150 | 149 | seqeq3d 13920 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ seq1( + , (๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐))))) = seq1( + , (๐ โ โ โฆ 0))) |
151 | 150 | rneqd 5894 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ ran seq1( + ,
(๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐))))) = ran seq1( + , (๐ โ โ โฆ 0))) |
152 | 151 | supeq1d 9387 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ sup(ran seq1( + ,
(๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐))))), โ*, < ) = sup(ran
seq1( + , (๐ โ โ
โฆ 0)), โ*, < )) |
153 | | 0cn 11152 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 0 โ
โ |
154 | | ser1const 13970 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((0
โ โ โง ๐
โ โ) โ (seq1( + , (โ ร {0}))โ๐) = (๐ ยท 0)) |
155 | 153, 154 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (seq1( +
, (โ ร {0}))โ๐) = (๐ ยท 0)) |
156 | | nncn 12166 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
โ) |
157 | 156 | mul01d 11359 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (๐ ยท 0) =
0) |
158 | 155, 157 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (seq1( +
, (โ ร {0}))โ๐) = 0) |
159 | 158 | mpteq2ia 5209 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โฆ (seq1( +
, (โ ร {0}))โ๐)) = (๐ โ โ โฆ 0) |
160 | | fconstmpt 5695 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โ
ร {0}) = (๐ โ
โ โฆ 0) |
161 | | seqeq3 13917 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((โ
ร {0}) = (๐ โ
โ โฆ 0) โ seq1( + , (โ ร {0})) = seq1( + , (๐ โ โ โฆ
0))) |
162 | 160, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข seq1( + ,
(โ ร {0})) = seq1( + , (๐ โ โ โฆ 0)) |
163 | | 1z 12538 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
โค |
164 | | seqfn 13924 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (1 โ
โค โ seq1( + , (โ ร {0})) Fn
(โคโฅโ1)) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
โข seq1( + ,
(โ ร {0})) Fn (โคโฅโ1) |
166 | | nnuz 12811 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข โ =
(โคโฅโ1) |
167 | 166 | fneq2i 6601 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (seq1( +
, (โ ร {0})) Fn โ โ seq1( + , (โ ร {0})) Fn
(โคโฅโ1)) |
168 | | dffn5 6902 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (seq1( +
, (โ ร {0})) Fn โ โ seq1( + , (โ ร {0})) =
(๐ โ โ โฆ
(seq1( + , (โ ร {0}))โ๐))) |
169 | 167, 168 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . 21
โข (seq1( +
, (โ ร {0})) Fn (โคโฅโ1) โ seq1( + ,
(โ ร {0})) = (๐
โ โ โฆ (seq1( + , (โ ร {0}))โ๐))) |
170 | 165, 169 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . 20
โข seq1( + ,
(โ ร {0})) = (๐
โ โ โฆ (seq1( + , (โ ร {0}))โ๐)) |
171 | 162, 170 | eqtr3i 2763 |
. . . . . . . . . . . . . . . . . . 19
โข seq1( + ,
(๐ โ โ โฆ
0)) = (๐ โ โ
โฆ (seq1( + , (โ ร {0}))โ๐)) |
172 | | fconstmpt 5695 |
. . . . . . . . . . . . . . . . . . 19
โข (โ
ร {0}) = (๐ โ
โ โฆ 0) |
173 | 159, 171,
172 | 3eqtr4i 2771 |
. . . . . . . . . . . . . . . . . 18
โข seq1( + ,
(๐ โ โ โฆ
0)) = (โ ร {0}) |
174 | 173 | rneqi 5893 |
. . . . . . . . . . . . . . . . 17
โข ran seq1(
+ , (๐ โ โ
โฆ 0)) = ran (โ ร {0}) |
175 | | 1nn 12169 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
176 | | ne0i 4295 |
. . . . . . . . . . . . . . . . . 18
โข (1 โ
โ โ โ โ โ
) |
177 | | rnxp 6123 |
. . . . . . . . . . . . . . . . . 18
โข (โ
โ โ
โ ran (โ ร {0}) = {0}) |
178 | 175, 176,
177 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
โข ran
(โ ร {0}) = {0} |
179 | 174, 178 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
โข ran seq1(
+ , (๐ โ โ
โฆ 0)) = {0} |
180 | 179 | supeq1i 9388 |
. . . . . . . . . . . . . . 15
โข sup(ran
seq1( + , (๐ โ โ
โฆ 0)), โ*, < ) = sup({0}, โ*, <
) |
181 | | xrltso 13066 |
. . . . . . . . . . . . . . . 16
โข < Or
โ* |
182 | | 0xr 11207 |
. . . . . . . . . . . . . . . 16
โข 0 โ
โ* |
183 | | supsn 9413 |
. . . . . . . . . . . . . . . 16
โข (( <
Or โ* โง 0 โ โ*) โ sup({0},
โ*, < ) = 0) |
184 | 181, 182,
183 | mp2an 691 |
. . . . . . . . . . . . . . 15
โข sup({0},
โ*, < ) = 0 |
185 | 180, 184 | eqtri 2761 |
. . . . . . . . . . . . . 14
โข sup(ran
seq1( + , (๐ โ โ
โฆ 0)), โ*, < ) = 0 |
186 | 152, 185 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ sup(ran seq1( + ,
(๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐))))), โ*, < ) =
0) |
187 | 186 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ sup(ran seq1( + , (๐ โ โ โฆ
(volโ((๐โ๐) โ โช ๐ โ (1..^๐)(๐โ๐))))), โ*, < ) =
0) |
188 | 124, 133,
187 | 3eqtr3rd 2782 |
. . . . . . . . . . 11
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ 0 = (volโโช ๐ด)) |
189 | 188 | ex 414 |
. . . . . . . . . 10
โข (๐:โโontoโ๐ด โ (โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ 0 = (volโโช ๐ด))) |
190 | 38, 189 | sylbid 239 |
. . . . . . . . 9
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ 0 =
(volโโช ๐ด))) |
191 | 28, 190 | syl5 34 |
. . . . . . . 8
โข (๐:โโontoโ๐ด โ ((โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ) โ 0 = (volโโช ๐ด))) |
192 | 191 | exlimiv 1934 |
. . . . . . 7
โข
(โ๐ ๐:โโontoโ๐ด โ ((โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ) โ 0 = (volโโช ๐ด))) |
193 | 18, 192 | syl 17 |
. . . . . 6
โข ((๐ด โ โ
โง ๐ด โผ โ) โ
((โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ) โ 0 = (volโโช ๐ด))) |
194 | 193 | expimpd 455 |
. . . . 5
โข (๐ด โ โ
โ ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (volโโช ๐ด))) |
195 | 11, 194 | pm2.61ine 3025 |
. . . 4
โข ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (volโโช ๐ด)) |
196 | | renepnf 11208 |
. . . . . . 7
โข (0 โ
โ โ 0 โ +โ) |
197 | 47, 196 | mp1i 13 |
. . . . . 6
โข (โช ๐ด =
โ โ 0 โ +โ) |
198 | | fveq2 6843 |
. . . . . . 7
โข (โช ๐ด =
โ โ (volโโช ๐ด) = (volโโ)) |
199 | | rembl 24920 |
. . . . . . . . 9
โข โ
โ dom vol |
200 | | mblvol 24910 |
. . . . . . . . 9
โข (โ
โ dom vol โ (volโโ) =
(vol*โโ)) |
201 | 199, 200 | ax-mp 5 |
. . . . . . . 8
โข
(volโโ) = (vol*โโ) |
202 | | ovolre 24905 |
. . . . . . . 8
โข
(vol*โโ) = +โ |
203 | 201, 202 | eqtri 2761 |
. . . . . . 7
โข
(volโโ) = +โ |
204 | 198, 203 | eqtrdi 2789 |
. . . . . 6
โข (โช ๐ด =
โ โ (volโโช ๐ด) = +โ) |
205 | 197, 204 | neeqtrrd 3015 |
. . . . 5
โข (โช ๐ด =
โ โ 0 โ (volโโช ๐ด)) |
206 | 205 | necon2i 2975 |
. . . 4
โข (0 =
(volโโช ๐ด) โ โช ๐ด โ โ) |
207 | 195, 206 | syl 17 |
. . 3
โข ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ โช ๐ด โ โ) |
208 | 207 | expr 458 |
. 2
โข ((๐ด โผ โ โง
โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ (โช ๐ด
โ โ โ โช ๐ด โ โ)) |
209 | | eqimss 4001 |
. . 3
โข (โช ๐ด =
โ โ โช ๐ด โ โ) |
210 | 209 | necon3bi 2967 |
. 2
โข (ยฌ
โช ๐ด โ โ โ โช ๐ด
โ โ) |
211 | 208, 210 | pm2.61d1 180 |
1
โข ((๐ด โผ โ โง
โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โช ๐ด
โ โ) |