Metamath Proof Explorer

Theorem voliune

Description: The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +oo for the measure of any set in the sum. Cf. ovoliun and voliun . (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion voliune 
|- ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) <-> ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) )
2 eqid 
 |-  seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) = seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) )
3 eqid 
 |-  ( n e. NN |-> ( vol ` A ) ) = ( n e. NN |-> ( vol ` A ) )
4 2 3 voliun 
 |-  ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
5 1 4 sylanbr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
6 5 an32s 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
7 nfra1 
 |-  F/ n A. n e. NN A e. dom vol
8 nfra1 
 |-  F/ n A. n e. NN ( vol ` A ) e. RR
9 7 8 nfan 
 |-  F/ n ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR )
10 simpr 
 |-  ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> n e. NN )
11 rspa 
 |-  ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> A e. dom vol )
12 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
13 12 ffvelcdmi 
 |-  ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
14 11 13 syl 
 |-  ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) )
15 3 fvmpt2 
 |-  ( ( n e. NN /\ ( vol ` A ) e. ( 0 [,] +oo ) ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) )
16 10 14 15 syl2anc 
 |-  ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) )
17 16 adantlr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) )
18 17 ex 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> ( n e. NN -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) )
19 9 18 ralrimi 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> A. n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) )
20 9 19 esumeq2d 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sum* n e. NN ( vol ` A ) )
21 simpr 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> A. n e. NN ( vol ` A ) e. RR )
22 21 r19.21bi 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. RR )
23 14 adantlr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) )
24 0xr 
 |-  0 e. RR*
25 pnfxr 
 |-  +oo e. RR*
26 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( vol ` A ) e. ( 0 [,] +oo ) <-> ( ( vol ` A ) e. RR* /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) <_ +oo ) ) )
27 24 25 26 mp2an 
 |-  ( ( vol ` A ) e. ( 0 [,] +oo ) <-> ( ( vol ` A ) e. RR* /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) <_ +oo ) )
28 27 simp2bi 
 |-  ( ( vol ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( vol ` A ) )
29 23 28 syl 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> 0 <_ ( vol ` A ) )
30 ltpnf 
 |-  ( ( vol ` A ) e. RR -> ( vol ` A ) < +oo )
31 22 30 syl 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) < +oo )
32 0re 
 |-  0 e. RR
33 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( vol ` A ) e. ( 0 [,) +oo ) <-> ( ( vol ` A ) e. RR /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) < +oo ) ) )
34 32 25 33 mp2an 
 |-  ( ( vol ` A ) e. ( 0 [,) +oo ) <-> ( ( vol ` A ) e. RR /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) < +oo ) )
35 22 29 31 34 syl3anbrc 
 |-  ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,) +oo ) )
36 9 35 3 fmptdf 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> ( n e. NN |-> ( vol ` A ) ) : NN --> ( 0 [,) +oo ) )
37 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( vol ` A ) )
38 37 esumfsupre 
 |-  ( ( n e. NN |-> ( vol ` A ) ) : NN --> ( 0 [,) +oo ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
39 36 38 syl 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
40 20 39 eqtr3d 
 |-  ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( vol ` A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
41 40 adantlr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( vol ` A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) )
42 6 41 eqtr4d 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) )
43 nfv 
 |-  F/ k ( vol ` A ) = +oo
44 nfcv 
 |-  F/_ n vol
45 nfcsb1v 
 |-  F/_ n [_ k / n ]_ A
46 44 45 nffv 
 |-  F/_ n ( vol ` [_ k / n ]_ A )
47 46 nfeq1 
 |-  F/ n ( vol ` [_ k / n ]_ A ) = +oo
48 csbeq1a 
 |-  ( n = k -> A = [_ k / n ]_ A )
49 48 fveqeq2d 
 |-  ( n = k -> ( ( vol ` A ) = +oo <-> ( vol ` [_ k / n ]_ A ) = +oo ) )
50 43 47 49 cbvrexw 
 |-  ( E. n e. NN ( vol ` A ) = +oo <-> E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo )
51 50 bilani 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo )
52 45 nfel1 
 |-  F/ n [_ k / n ]_ A e. dom vol
53 48 eleq1d 
 |-  ( n = k -> ( A e. dom vol <-> [_ k / n ]_ A e. dom vol ) )
54 52 53 rspc 
 |-  ( k e. NN -> ( A. n e. NN A e. dom vol -> [_ k / n ]_ A e. dom vol ) )
55 54 impcom 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A e. dom vol )
56 iunmbl 
 |-  ( A. n e. NN A e. dom vol -> U_ n e. NN A e. dom vol )
57 56 adantr 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> U_ n e. NN A e. dom vol )
58 nfcv 
 |-  F/_ n NN
59 nfcv 
 |-  F/_ n k
60 58 59 45 48 ssiun2sf 
 |-  ( k e. NN -> [_ k / n ]_ A C_ U_ n e. NN A )
61 60 adantl 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A C_ U_ n e. NN A )
62 volss 
 |-  ( ( [_ k / n ]_ A e. dom vol /\ U_ n e. NN A e. dom vol /\ [_ k / n ]_ A C_ U_ n e. NN A ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
63 55 57 61 62 syl3anc 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
64 63 adantlr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
65 64 adantlr 
 |-  ( ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
66 65 ralrimiva 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> A. k e. NN ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
67 r19.29r 
 |-  ( ( E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo /\ A. k e. NN ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) )
68 51 66 67 syl2anc 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) )
69 breq1 
 |-  ( ( vol ` [_ k / n ]_ A ) = +oo -> ( ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) <-> +oo <_ ( vol ` U_ n e. NN A ) ) )
70 69 biimpa 
 |-  ( ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> +oo <_ ( vol ` U_ n e. NN A ) )
71 70 reximi 
 |-  ( E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) )
72 68 71 syl 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) )
73 1nn 
 |-  1 e. NN
74 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
75 r19.9rzv 
 |-  ( NN =/= (/) -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) )
76 73 74 75 mp2b 
 |-  ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) )
77 72 76 sylibr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> +oo <_ ( vol ` U_ n e. NN A ) )
78 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
79 12 ffvelcdmi 
 |-  ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. ( 0 [,] +oo ) )
80 78 79 sselid 
 |-  ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* )
81 56 80 syl 
 |-  ( A. n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* )
82 81 ad2antrr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) e. RR* )
83 xgepnf 
 |-  ( ( vol ` U_ n e. NN A ) e. RR* -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> ( vol ` U_ n e. NN A ) = +oo ) )
84 82 83 syl 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> ( vol ` U_ n e. NN A ) = +oo ) )
85 77 84 mpbid 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) = +oo )
86 nfdisj1 
 |-  F/ n Disj_ n e. NN A
87 7 86 nfan 
 |-  F/ n ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A )
88 nfre1 
 |-  F/ n E. n e. NN ( vol ` A ) = +oo
89 87 88 nfan 
 |-  F/ n ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo )
90 nnex 
 |-  NN e. _V
91 90 a1i 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> NN e. _V )
92 14 3ad2antr3 
 |-  ( ( A. n e. NN A e. dom vol /\ ( Disj_ n e. NN A /\ E. n e. NN ( vol ` A ) = +oo /\ n e. NN ) ) -> ( vol ` A ) e. ( 0 [,] +oo ) )
93 92 3anassrs 
 |-  ( ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) )
94 simpr 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. n e. NN ( vol ` A ) = +oo )
95 89 91 93 94 esumpinfval 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> sum* n e. NN ( vol ` A ) = +oo )
96 85 95 eqtr4d 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) )
97 exmid 
 |-  ( A. n e. NN ( vol ` A ) e. RR \/ -. A. n e. NN ( vol ` A ) e. RR )
98 rexnal 
 |-  ( E. n e. NN -. ( vol ` A ) e. RR <-> -. A. n e. NN ( vol ` A ) e. RR )
99 98 orbi2i 
 |-  ( ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR ) <-> ( A. n e. NN ( vol ` A ) e. RR \/ -. A. n e. NN ( vol ` A ) e. RR ) )
100 97 99 mpbir 
 |-  ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR )
101 r19.29 
 |-  ( ( A. n e. NN A e. dom vol /\ E. n e. NN -. ( vol ` A ) e. RR ) -> E. n e. NN ( A e. dom vol /\ -. ( vol ` A ) e. RR ) )
102 xrge0nre 
 |-  ( ( ( vol ` A ) e. ( 0 [,] +oo ) /\ -. ( vol ` A ) e. RR ) -> ( vol ` A ) = +oo )
103 13 102 sylan 
 |-  ( ( A e. dom vol /\ -. ( vol ` A ) e. RR ) -> ( vol ` A ) = +oo )
104 103 reximi 
 |-  ( E. n e. NN ( A e. dom vol /\ -. ( vol ` A ) e. RR ) -> E. n e. NN ( vol ` A ) = +oo )
105 101 104 syl 
 |-  ( ( A. n e. NN A e. dom vol /\ E. n e. NN -. ( vol ` A ) e. RR ) -> E. n e. NN ( vol ` A ) = +oo )
106 105 ex 
 |-  ( A. n e. NN A e. dom vol -> ( E. n e. NN -. ( vol ` A ) e. RR -> E. n e. NN ( vol ` A ) = +oo ) )
107 106 orim2d 
 |-  ( A. n e. NN A e. dom vol -> ( ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR ) -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) ) )
108 100 107 mpi 
 |-  ( A. n e. NN A e. dom vol -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) )
109 108 adantr 
 |-  ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) )
110 42 96 109 mpjaodan 
 |-  ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) )