Step |
Hyp |
Ref |
Expression |
1 |
|
volf |
|- vol : dom vol --> ( 0 [,] +oo ) |
2 |
|
fvssunirn |
|- ( sigAlgebra ` RR ) C_ U. ran sigAlgebra |
3 |
|
dmvlsiga |
|- dom vol e. ( sigAlgebra ` RR ) |
4 |
2 3
|
sselii |
|- dom vol e. U. ran sigAlgebra |
5 |
|
0elsiga |
|- ( dom vol e. U. ran sigAlgebra -> (/) e. dom vol ) |
6 |
4 5
|
ax-mp |
|- (/) e. dom vol |
7 |
|
mblvol |
|- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) ) |
8 |
6 7
|
ax-mp |
|- ( vol ` (/) ) = ( vol* ` (/) ) |
9 |
|
ovol0 |
|- ( vol* ` (/) ) = 0 |
10 |
8 9
|
eqtri |
|- ( vol ` (/) ) = 0 |
11 |
|
simpr |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> x e. Fin ) |
12 |
|
nfv |
|- F/ y x e. ~P dom vol |
13 |
|
nfv |
|- F/ y x ~<_ _om |
14 |
|
nfdisj1 |
|- F/ y Disj_ y e. x y |
15 |
13 14
|
nfan |
|- F/ y ( x ~<_ _om /\ Disj_ y e. x y ) |
16 |
12 15
|
nfan |
|- F/ y ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) |
17 |
|
nfv |
|- F/ y x e. Fin |
18 |
16 17
|
nfan |
|- F/ y ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) |
19 |
|
elpwi |
|- ( x e. ~P dom vol -> x C_ dom vol ) |
20 |
19
|
ad3antrrr |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> x C_ dom vol ) |
21 |
|
simpr |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> y e. x ) |
22 |
20 21
|
sseldd |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> y e. dom vol ) |
23 |
22
|
ex |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> ( y e. x -> y e. dom vol ) ) |
24 |
18 23
|
ralrimi |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> A. y e. x y e. dom vol ) |
25 |
|
simplrr |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> Disj_ y e. x y ) |
26 |
|
uniiun |
|- U. x = U_ y e. x y |
27 |
26
|
fveq2i |
|- ( vol ` U. x ) = ( vol ` U_ y e. x y ) |
28 |
|
volfiniune |
|- ( ( x e. Fin /\ A. y e. x y e. dom vol /\ Disj_ y e. x y ) -> ( vol ` U_ y e. x y ) = sum* y e. x ( vol ` y ) ) |
29 |
27 28
|
syl5eq |
|- ( ( x e. Fin /\ A. y e. x y e. dom vol /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
30 |
11 24 25 29
|
syl3anc |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
31 |
|
bren |
|- ( NN ~~ x <-> E. f f : NN -1-1-onto-> x ) |
32 |
|
nfv |
|- F/ n ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) |
33 |
|
nfcv |
|- F/_ n ( vol ` y ) |
34 |
|
nfcv |
|- F/_ y ( vol ` ( f ` n ) ) |
35 |
|
nfcv |
|- F/_ n x |
36 |
|
nfcv |
|- F/_ n NN |
37 |
|
nfcv |
|- F/_ n f |
38 |
|
fveq2 |
|- ( y = ( f ` n ) -> ( vol ` y ) = ( vol ` ( f ` n ) ) ) |
39 |
|
simpl |
|- ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> x e. ~P dom vol ) |
40 |
|
simpr |
|- ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> f : NN -1-1-onto-> x ) |
41 |
|
eqidd |
|- ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) = ( f ` n ) ) |
42 |
1
|
a1i |
|- ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> vol : dom vol --> ( 0 [,] +oo ) ) |
43 |
39 19
|
syl |
|- ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> x C_ dom vol ) |
44 |
43
|
sselda |
|- ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> y e. dom vol ) |
45 |
42 44
|
ffvelrnd |
|- ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> ( vol ` y ) e. ( 0 [,] +oo ) ) |
46 |
32 33 34 35 36 37 38 39 40 41 45
|
esumf1o |
|- ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> sum* y e. x ( vol ` y ) = sum* n e. NN ( vol ` ( f ` n ) ) ) |
47 |
46
|
adantlr |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> sum* y e. x ( vol ` y ) = sum* n e. NN ( vol ` ( f ` n ) ) ) |
48 |
19
|
ad3antrrr |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> x C_ dom vol ) |
49 |
|
f1of |
|- ( f : NN -1-1-onto-> x -> f : NN --> x ) |
50 |
49
|
adantl |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> f : NN --> x ) |
51 |
50
|
ffvelrnda |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) e. x ) |
52 |
48 51
|
sseldd |
|- ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) e. dom vol ) |
53 |
52
|
ralrimiva |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> A. n e. NN ( f ` n ) e. dom vol ) |
54 |
|
simpr |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> f : NN -1-1-onto-> x ) |
55 |
|
simplrr |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> Disj_ y e. x y ) |
56 |
|
id |
|- ( f : NN -1-1-onto-> x -> f : NN -1-1-onto-> x ) |
57 |
|
simpr |
|- ( ( f : NN -1-1-onto-> x /\ y = ( f ` n ) ) -> y = ( f ` n ) ) |
58 |
56 57
|
disjrdx |
|- ( f : NN -1-1-onto-> x -> ( Disj_ n e. NN ( f ` n ) <-> Disj_ y e. x y ) ) |
59 |
58
|
biimpar |
|- ( ( f : NN -1-1-onto-> x /\ Disj_ y e. x y ) -> Disj_ n e. NN ( f ` n ) ) |
60 |
54 55 59
|
syl2anc |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> Disj_ n e. NN ( f ` n ) ) |
61 |
|
voliune |
|- ( ( A. n e. NN ( f ` n ) e. dom vol /\ Disj_ n e. NN ( f ` n ) ) -> ( vol ` U_ n e. NN ( f ` n ) ) = sum* n e. NN ( vol ` ( f ` n ) ) ) |
62 |
53 60 61
|
syl2anc |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U_ n e. NN ( f ` n ) ) = sum* n e. NN ( vol ` ( f ` n ) ) ) |
63 |
|
f1ofo |
|- ( f : NN -1-1-onto-> x -> f : NN -onto-> x ) |
64 |
63 57
|
iunrdx |
|- ( f : NN -1-1-onto-> x -> U_ n e. NN ( f ` n ) = U_ y e. x y ) |
65 |
64 26
|
eqtr4di |
|- ( f : NN -1-1-onto-> x -> U_ n e. NN ( f ` n ) = U. x ) |
66 |
65
|
fveq2d |
|- ( f : NN -1-1-onto-> x -> ( vol ` U_ n e. NN ( f ` n ) ) = ( vol ` U. x ) ) |
67 |
66
|
adantl |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U_ n e. NN ( f ` n ) ) = ( vol ` U. x ) ) |
68 |
47 62 67
|
3eqtr2rd |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
69 |
68
|
ex |
|- ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( f : NN -1-1-onto-> x -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) |
70 |
69
|
exlimdv |
|- ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( E. f f : NN -1-1-onto-> x -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) |
71 |
70
|
imp |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ E. f f : NN -1-1-onto-> x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
72 |
31 71
|
sylan2b |
|- ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ NN ~~ x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
73 |
|
brdom2 |
|- ( x ~<_ _om <-> ( x ~< _om \/ x ~~ _om ) ) |
74 |
73
|
biimpi |
|- ( x ~<_ _om -> ( x ~< _om \/ x ~~ _om ) ) |
75 |
|
isfinite2 |
|- ( x ~< _om -> x e. Fin ) |
76 |
|
ensymb |
|- ( x ~~ _om <-> _om ~~ x ) |
77 |
|
nnenom |
|- NN ~~ _om |
78 |
|
entr |
|- ( ( NN ~~ _om /\ _om ~~ x ) -> NN ~~ x ) |
79 |
77 78
|
mpan |
|- ( _om ~~ x -> NN ~~ x ) |
80 |
76 79
|
sylbi |
|- ( x ~~ _om -> NN ~~ x ) |
81 |
75 80
|
orim12i |
|- ( ( x ~< _om \/ x ~~ _om ) -> ( x e. Fin \/ NN ~~ x ) ) |
82 |
74 81
|
syl |
|- ( x ~<_ _om -> ( x e. Fin \/ NN ~~ x ) ) |
83 |
82
|
ad2antrl |
|- ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( x e. Fin \/ NN ~~ x ) ) |
84 |
30 72 83
|
mpjaodan |
|- ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
85 |
84
|
ex |
|- ( x e. ~P dom vol -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) |
86 |
85
|
rgen |
|- A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) |
87 |
|
ismeas |
|- ( dom vol e. U. ran sigAlgebra -> ( vol e. ( measures ` dom vol ) <-> ( vol : dom vol --> ( 0 [,] +oo ) /\ ( vol ` (/) ) = 0 /\ A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) ) ) |
88 |
4 87
|
ax-mp |
|- ( vol e. ( measures ` dom vol ) <-> ( vol : dom vol --> ( 0 [,] +oo ) /\ ( vol ` (/) ) = 0 /\ A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) ) |
89 |
1 10 86 88
|
mpbir3an |
|- vol e. ( measures ` dom vol ) |