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 ffvelrni 
 |-  ( 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 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 )
44 nfv 
 |-  F/ k ( vol ` A ) = +oo
45 nfcv 
 |-  F/_ n vol
46 nfcsb1v 
 |-  F/_ n [_ k / n ]_ A
47 45 46 nffv 
 |-  F/_ n ( vol ` [_ k / n ]_ A )
48 47 nfeq1 
 |-  F/ n ( vol ` [_ k / n ]_ A ) = +oo
49 csbeq1a 
 |-  ( n = k -> A = [_ k / n ]_ A )
50 49 fveqeq2d 
 |-  ( n = k -> ( ( vol ` A ) = +oo <-> ( vol ` [_ k / n ]_ A ) = +oo ) )
51 44 48 50 cbvrexw 
 |-  ( E. n e. NN ( vol ` A ) = +oo <-> E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo )
52 43 51 sylib 
 |-  ( ( ( 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 )
53 46 nfel1 
 |-  F/ n [_ k / n ]_ A e. dom vol
54 49 eleq1d 
 |-  ( n = k -> ( A e. dom vol <-> [_ k / n ]_ A e. dom vol ) )
55 53 54 rspc 
 |-  ( k e. NN -> ( A. n e. NN A e. dom vol -> [_ k / n ]_ A e. dom vol ) )
56 55 impcom 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A e. dom vol )
57 iunmbl 
 |-  ( A. n e. NN A e. dom vol -> U_ n e. NN A e. dom vol )
58 57 adantr 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> U_ n e. NN A e. dom vol )
59 nfcv 
 |-  F/_ n NN
60 nfcv 
 |-  F/_ n k
61 59 60 46 49 ssiun2sf 
 |-  ( k e. NN -> [_ k / n ]_ A C_ U_ n e. NN A )
62 61 adantl 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A C_ U_ n e. NN A )
63 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 ) )
64 56 58 62 63 syl3anc 
 |-  ( ( A. n e. NN A e. dom vol /\ 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 ) /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) )
66 65 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 ) )
67 66 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 ) )
68 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 ) ) )
69 52 67 68 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 ) ) )
70 breq1 
 |-  ( ( vol ` [_ k / n ]_ A ) = +oo -> ( ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) <-> +oo <_ ( vol ` U_ n e. NN A ) ) )
71 70 biimpa 
 |-  ( ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> +oo <_ ( vol ` U_ n e. NN A ) )
72 71 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 ) )
73 69 72 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 ) )
74 1nn 
 |-  1 e. NN
75 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
76 r19.9rzv 
 |-  ( NN =/= (/) -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) )
77 74 75 76 mp2b 
 |-  ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) )
78 73 77 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 ) )
79 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
80 12 ffvelrni 
 |-  ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. ( 0 [,] +oo ) )
81 79 80 sseldi 
 |-  ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* )
82 57 81 syl 
 |-  ( A. n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* )
83 82 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* )
84 xgepnf 
 |-  ( ( vol ` U_ n e. NN A ) e. RR* -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> ( vol ` U_ n e. NN A ) = +oo ) )
85 83 84 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 ) )
86 78 85 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 )
87 nfdisj1 
 |-  F/ n Disj_ n e. NN A
88 7 87 nfan 
 |-  F/ n ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A )
89 nfre1 
 |-  F/ n E. n e. NN ( vol ` A ) = +oo
90 88 89 nfan 
 |-  F/ n ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo )
91 nnex 
 |-  NN e. _V
92 91 a1i 
 |-  ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> NN e. _V )
93 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 ) )
94 93 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 ) )
95 90 92 94 43 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 86 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 ) )