Step | Hyp | Ref
| Expression |
1 | | volf 24909 |
. 2
β’ vol:dom
volβΆ(0[,]+β) |
2 | | fvssunirn 6876 |
. . . . . 6
β’
(sigAlgebraββ) β βͺ ran
sigAlgebra |
3 | | dmvlsiga 32785 |
. . . . . 6
β’ dom vol
β (sigAlgebraββ) |
4 | 2, 3 | sselii 3942 |
. . . . 5
β’ dom vol
β βͺ ran sigAlgebra |
5 | | 0elsiga 32770 |
. . . . 5
β’ (dom vol
β βͺ ran sigAlgebra β β
β dom
vol) |
6 | 4, 5 | ax-mp 5 |
. . . 4
β’ β
β dom vol |
7 | | mblvol 24910 |
. . . 4
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
8 | 6, 7 | ax-mp 5 |
. . 3
β’
(volββ
) = (vol*ββ
) |
9 | | ovol0 24873 |
. . 3
β’
(vol*ββ
) = 0 |
10 | 8, 9 | eqtri 2761 |
. 2
β’
(volββ
) = 0 |
11 | | simpr 486 |
. . . . . 6
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β π₯ β Fin) |
12 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦ π₯ β π« dom
vol |
13 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦ π₯ βΌ
Ο |
14 | | nfdisj1 5085 |
. . . . . . . . . 10
β’
β²π¦Disj
π¦ β π₯ π¦ |
15 | 13, 14 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦) |
16 | 12, 15 | nfan 1903 |
. . . . . . . 8
β’
β²π¦(π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) |
17 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦ π₯ β Fin |
18 | 16, 17 | nfan 1903 |
. . . . . . 7
β’
β²π¦((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) |
19 | | elpwi 4568 |
. . . . . . . . . 10
β’ (π₯ β π« dom vol β
π₯ β dom
vol) |
20 | 19 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β§ π¦ β π₯) β π₯ β dom vol) |
21 | | simpr 486 |
. . . . . . . . 9
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β§ π¦ β π₯) β π¦ β π₯) |
22 | 20, 21 | sseldd 3946 |
. . . . . . . 8
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β§ π¦ β π₯) β π¦ β dom vol) |
23 | 22 | ex 414 |
. . . . . . 7
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β (π¦ β π₯ β π¦ β dom vol)) |
24 | 18, 23 | ralrimi 3239 |
. . . . . 6
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β βπ¦ β π₯ π¦ β dom vol) |
25 | | simplrr 777 |
. . . . . 6
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β Disj π¦ β π₯ π¦) |
26 | | uniiun 5019 |
. . . . . . . 8
β’ βͺ π₯ =
βͺ π¦ β π₯ π¦ |
27 | 26 | fveq2i 6846 |
. . . . . . 7
β’
(volββͺ π₯) = (volββͺ π¦ β π₯ π¦) |
28 | | volfiniune 32886 |
. . . . . . 7
β’ ((π₯ β Fin β§ βπ¦ β π₯ π¦ β dom vol β§ Disj π¦ β π₯ π¦) β (volββͺ π¦ β π₯ π¦) = Ξ£*π¦ β π₯(volβπ¦)) |
29 | 27, 28 | eqtrid 2785 |
. . . . . 6
β’ ((π₯ β Fin β§ βπ¦ β π₯ π¦ β dom vol β§ Disj π¦ β π₯ π¦) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
30 | 11, 24, 25, 29 | syl3anc 1372 |
. . . . 5
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π₯ β Fin) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
31 | | bren 8896 |
. . . . . 6
β’ (β
β π₯ β
βπ π:ββ1-1-ontoβπ₯) |
32 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π(π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) |
33 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(volβπ¦) |
34 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π¦(volβ(πβπ)) |
35 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ₯ |
36 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²πβ |
37 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ |
38 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ) β (volβπ¦) = (volβ(πβπ))) |
39 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β π₯ β π« dom vol) |
40 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β π:ββ1-1-ontoβπ₯) |
41 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β§ π β β) β (πβπ) = (πβπ)) |
42 | 1 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β§ π¦ β π₯) β vol:dom
volβΆ(0[,]+β)) |
43 | 39, 19 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β π₯ β dom vol) |
44 | 43 | sselda 3945 |
. . . . . . . . . . . . 13
β’ (((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β§ π¦ β π₯) β π¦ β dom vol) |
45 | 42, 44 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ (((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β§ π¦ β π₯) β (volβπ¦) β (0[,]+β)) |
46 | 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 45 | esumf1o 32706 |
. . . . . . . . . . 11
β’ ((π₯ β π« dom vol β§
π:ββ1-1-ontoβπ₯) β Ξ£*π¦ β π₯(volβπ¦) = Ξ£*π β β(volβ(πβπ))) |
47 | 46 | adantlr 714 |
. . . . . . . . . 10
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β
Ξ£*π¦ β
π₯(volβπ¦) = Ξ£*π β β(volβ(πβπ))) |
48 | 19 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β§ π β β) β π₯ β dom vol) |
49 | | f1of 6785 |
. . . . . . . . . . . . . . 15
β’ (π:ββ1-1-ontoβπ₯ β π:ββΆπ₯) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β π:ββΆπ₯) |
51 | 50 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β§ π β β) β (πβπ) β π₯) |
52 | 48, 51 | sseldd 3946 |
. . . . . . . . . . . 12
β’ ((((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β§ π β β) β (πβπ) β dom vol) |
53 | 52 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β βπ β β (πβπ) β dom vol) |
54 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β π:ββ1-1-ontoβπ₯) |
55 | | simplrr 777 |
. . . . . . . . . . . 12
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β Disj π¦ β π₯ π¦) |
56 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π:ββ1-1-ontoβπ₯ β π:ββ1-1-ontoβπ₯) |
57 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π:ββ1-1-ontoβπ₯ β§ π¦ = (πβπ)) β π¦ = (πβπ)) |
58 | 56, 57 | disjrdx 31555 |
. . . . . . . . . . . . 13
β’ (π:ββ1-1-ontoβπ₯ β (Disj π β β (πβπ) β Disj π¦ β π₯ π¦)) |
59 | 58 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π:ββ1-1-ontoβπ₯ β§ Disj π¦ β π₯ π¦) β Disj π β β (πβπ)) |
60 | 54, 55, 59 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β Disj π β β (πβπ)) |
61 | | voliune 32885 |
. . . . . . . . . . 11
β’
((βπ β
β (πβπ) β dom vol β§
Disj π β
β (πβπ)) β (volββͺ π β β (πβπ)) = Ξ£*π β β(volβ(πβπ))) |
62 | 53, 60, 61 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β (volββͺ π β β (πβπ)) = Ξ£*π β β(volβ(πβπ))) |
63 | | f1ofo 6792 |
. . . . . . . . . . . . . 14
β’ (π:ββ1-1-ontoβπ₯ β π:ββontoβπ₯) |
64 | 63, 57 | iunrdx 31528 |
. . . . . . . . . . . . 13
β’ (π:ββ1-1-ontoβπ₯ β βͺ π β β (πβπ) = βͺ π¦ β π₯ π¦) |
65 | 64, 26 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π:ββ1-1-ontoβπ₯ β βͺ π β β (πβπ) = βͺ π₯) |
66 | 65 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π:ββ1-1-ontoβπ₯ β (volββͺ π β β (πβπ)) = (volββͺ
π₯)) |
67 | 66 | adantl 483 |
. . . . . . . . . 10
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β (volββͺ π β β (πβπ)) = (volββͺ
π₯)) |
68 | 47, 62, 67 | 3eqtr2rd 2780 |
. . . . . . . . 9
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ π:ββ1-1-ontoβπ₯) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
69 | 68 | ex 414 |
. . . . . . . 8
β’ ((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β (π:ββ1-1-ontoβπ₯ β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦))) |
70 | 69 | exlimdv 1937 |
. . . . . . 7
β’ ((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β (βπ π:ββ1-1-ontoβπ₯ β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦))) |
71 | 70 | imp 408 |
. . . . . 6
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ βπ π:ββ1-1-ontoβπ₯) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
72 | 31, 71 | sylan2b 595 |
. . . . 5
β’ (((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β§ β β π₯) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
73 | | brdom2 8925 |
. . . . . . . 8
β’ (π₯ βΌ Ο β (π₯ βΊ Ο β¨ π₯ β
Ο)) |
74 | 73 | biimpi 215 |
. . . . . . 7
β’ (π₯ βΌ Ο β (π₯ βΊ Ο β¨ π₯ β
Ο)) |
75 | | isfinite2 9248 |
. . . . . . . 8
β’ (π₯ βΊ Ο β π₯ β Fin) |
76 | | ensymb 8945 |
. . . . . . . . 9
β’ (π₯ β Ο β Ο
β π₯) |
77 | | nnenom 13891 |
. . . . . . . . . 10
β’ β
β Ο |
78 | | entr 8949 |
. . . . . . . . . 10
β’ ((β
β Ο β§ Ο β π₯) β β β π₯) |
79 | 77, 78 | mpan 689 |
. . . . . . . . 9
β’ (Ο
β π₯ β β
β π₯) |
80 | 76, 79 | sylbi 216 |
. . . . . . . 8
β’ (π₯ β Ο β β
β π₯) |
81 | 75, 80 | orim12i 908 |
. . . . . . 7
β’ ((π₯ βΊ Ο β¨ π₯ β Ο) β (π₯ β Fin β¨ β β
π₯)) |
82 | 74, 81 | syl 17 |
. . . . . 6
β’ (π₯ βΌ Ο β (π₯ β Fin β¨ β β
π₯)) |
83 | 82 | ad2antrl 727 |
. . . . 5
β’ ((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β (π₯ β Fin β¨ β β π₯)) |
84 | 30, 72, 83 | mpjaodan 958 |
. . . 4
β’ ((π₯ β π« dom vol β§
(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦)) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
85 | 84 | ex 414 |
. . 3
β’ (π₯ β π« dom vol β
((π₯ βΌ Ο β§
Disj π¦ β π₯ π¦) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦))) |
86 | 85 | rgen 3063 |
. 2
β’
βπ₯ β
π« dom vol((π₯
βΌ Ο β§ Disj π¦ β π₯ π¦) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)) |
87 | | ismeas 32855 |
. . 3
β’ (dom vol
β βͺ ran sigAlgebra β (vol β
(measuresβdom vol) β (vol:dom volβΆ(0[,]+β) β§
(volββ
) = 0 β§ βπ₯ β π« dom vol((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦))))) |
88 | 4, 87 | ax-mp 5 |
. 2
β’ (vol
β (measuresβdom vol) β (vol:dom volβΆ(0[,]+β) β§
(volββ
) = 0 β§ βπ₯ β π« dom vol((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (volββͺ π₯) =
Ξ£*π¦ β
π₯(volβπ¦)))) |
89 | 1, 10, 86, 88 | mpbir3an 1342 |
1
β’ vol
β (measuresβdom vol) |