Metamath Proof Explorer

Theorem meascnbl

Description: A measure is continuous from below. Cf. volsup . (Contributed by Thierry Arnoux, 18-Jan-2017) (Revised by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses meascnbl.0 
|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
meascnbl.1 
|- ( ph -> M e. ( measures ` S ) )
meascnbl.2 
|- ( ph -> F : NN --> S )
meascnbl.3 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
Assertion meascnbl 
|- ( ph -> ( M o. F ) ( ~~>t ` J ) ( M ` U. ran F ) )

Proof

Step Hyp Ref Expression
1 meascnbl.0 
 |-  J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2 meascnbl.1 
 |-  ( ph -> M e. ( measures ` S ) )
3 meascnbl.2 
 |-  ( ph -> F : NN --> S )
4 meascnbl.3 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
5 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> M e. ( measures ` S ) )
6 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
7 2 6 syl 
 |-  ( ph -> S e. U. ran sigAlgebra )
8 7 adantr 
 |-  ( ( ph /\ n e. NN ) -> S e. U. ran sigAlgebra )
9 3 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. S )
10 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> ph )
11 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
12 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> k e. ( 1 ..^ n ) )
13 11 12 sselid 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> k e. NN )
14 3 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. S )
15 10 13 14 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> ( F ` k ) e. S )
16 15 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ( 1 ..^ n ) ( F ` k ) e. S )
17 sigaclfu2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ n ) ( F ` k ) e. S ) -> U_ k e. ( 1 ..^ n ) ( F ` k ) e. S )
18 8 16 17 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ..^ n ) ( F ` k ) e. S )
19 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ ( F ` n ) e. S /\ U_ k e. ( 1 ..^ n ) ( F ` k ) e. S ) -> ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) e. S )
20 8 9 18 19 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) e. S )
21 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) e. S ) -> ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) e. ( 0 [,] +oo ) )
22 5 20 21 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) e. ( 0 [,] +oo ) )
23 fveq2 
 |-  ( n = o -> ( F ` n ) = ( F ` o ) )
24 oveq2 
 |-  ( n = o -> ( 1 ..^ n ) = ( 1 ..^ o ) )
25 24 iuneq1d 
 |-  ( n = o -> U_ k e. ( 1 ..^ n ) ( F ` k ) = U_ k e. ( 1 ..^ o ) ( F ` k ) )
26 23 25 difeq12d 
 |-  ( n = o -> ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) = ( ( F ` o ) \ U_ k e. ( 1 ..^ o ) ( F ` k ) ) )
27 26 fveq2d 
 |-  ( n = o -> ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) = ( M ` ( ( F ` o ) \ U_ k e. ( 1 ..^ o ) ( F ` k ) ) ) )
28 fveq2 
 |-  ( n = p -> ( F ` n ) = ( F ` p ) )
29 oveq2 
 |-  ( n = p -> ( 1 ..^ n ) = ( 1 ..^ p ) )
30 29 iuneq1d 
 |-  ( n = p -> U_ k e. ( 1 ..^ n ) ( F ` k ) = U_ k e. ( 1 ..^ p ) ( F ` k ) )
31 28 30 difeq12d 
 |-  ( n = p -> ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) = ( ( F ` p ) \ U_ k e. ( 1 ..^ p ) ( F ` k ) ) )
32 31 fveq2d 
 |-  ( n = p -> ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) = ( M ` ( ( F ` p ) \ U_ k e. ( 1 ..^ p ) ( F ` k ) ) ) )
33 1 22 27 32 esumcvg2 
 |-  ( ph -> ( i e. NN |-> sum* n e. ( 1 ... i ) ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) ) ( ~~>t ` J ) sum* n e. NN ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) )
34 measfrge0 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
35 2 34 syl 
 |-  ( ph -> M : S --> ( 0 [,] +oo ) )
36 fcompt 
 |-  ( ( M : S --> ( 0 [,] +oo ) /\ F : NN --> S ) -> ( M o. F ) = ( i e. NN |-> ( M ` ( F ` i ) ) ) )
37 35 3 36 syl2anc 
 |-  ( ph -> ( M o. F ) = ( i e. NN |-> ( M ` ( F ` i ) ) ) )
38 nfcv 
 |-  F/_ n ( F ` k )
39 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
40 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
41 40 nnzd 
 |-  ( ( ph /\ i e. NN ) -> i e. ZZ )
42 fzval3 
 |-  ( i e. ZZ -> ( 1 ... i ) = ( 1 ..^ ( i + 1 ) ) )
43 41 42 syl 
 |-  ( ( ph /\ i e. NN ) -> ( 1 ... i ) = ( 1 ..^ ( i + 1 ) ) )
44 43 olcd 
 |-  ( ( ph /\ i e. NN ) -> ( ( 1 ... i ) = NN \/ ( 1 ... i ) = ( 1 ..^ ( i + 1 ) ) ) )
45 2 adantr 
 |-  ( ( ph /\ i e. NN ) -> M e. ( measures ` S ) )
46 simpll 
 |-  ( ( ( ph /\ i e. NN ) /\ n e. ( 1 ... i ) ) -> ph )
47 fzossnn 
 |-  ( 1 ..^ ( i + 1 ) ) C_ NN
48 43 eleq2d 
 |-  ( ( ph /\ i e. NN ) -> ( n e. ( 1 ... i ) <-> n e. ( 1 ..^ ( i + 1 ) ) ) )
49 48 biimpa 
 |-  ( ( ( ph /\ i e. NN ) /\ n e. ( 1 ... i ) ) -> n e. ( 1 ..^ ( i + 1 ) ) )
50 47 49 sselid 
 |-  ( ( ( ph /\ i e. NN ) /\ n e. ( 1 ... i ) ) -> n e. NN )
51 46 50 9 syl2anc 
 |-  ( ( ( ph /\ i e. NN ) /\ n e. ( 1 ... i ) ) -> ( F ` n ) e. S )
52 38 39 44 45 51 measiuns 
 |-  ( ( ph /\ i e. NN ) -> ( M ` U_ n e. ( 1 ... i ) ( F ` n ) ) = sum* n e. ( 1 ... i ) ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) )
53 3 ffnd 
 |-  ( ph -> F Fn NN )
54 53 4 iuninc 
 |-  ( ( ph /\ i e. NN ) -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) )
55 54 fveq2d 
 |-  ( ( ph /\ i e. NN ) -> ( M ` U_ n e. ( 1 ... i ) ( F ` n ) ) = ( M ` ( F ` i ) ) )
56 52 55 eqtr3d 
 |-  ( ( ph /\ i e. NN ) -> sum* n e. ( 1 ... i ) ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) = ( M ` ( F ` i ) ) )
57 56 mpteq2dva 
 |-  ( ph -> ( i e. NN |-> sum* n e. ( 1 ... i ) ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) ) = ( i e. NN |-> ( M ` ( F ` i ) ) ) )
58 37 57 eqtr4d 
 |-  ( ph -> ( M o. F ) = ( i e. NN |-> sum* n e. ( 1 ... i ) ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) ) )
59 9 ralrimiva 
 |-  ( ph -> A. n e. NN ( F ` n ) e. S )
60 dfiun2g 
 |-  ( A. n e. NN ( F ` n ) e. S -> U_ n e. NN ( F ` n ) = U. { x | E. n e. NN x = ( F ` n ) } )
61 59 60 syl 
 |-  ( ph -> U_ n e. NN ( F ` n ) = U. { x | E. n e. NN x = ( F ` n ) } )
62 fnrnfv 
 |-  ( F Fn NN -> ran F = { x | E. n e. NN x = ( F ` n ) } )
63 53 62 syl 
 |-  ( ph -> ran F = { x | E. n e. NN x = ( F ` n ) } )
64 63 unieqd 
 |-  ( ph -> U. ran F = U. { x | E. n e. NN x = ( F ` n ) } )
65 61 64 eqtr4d 
 |-  ( ph -> U_ n e. NN ( F ` n ) = U. ran F )
66 65 fveq2d 
 |-  ( ph -> ( M ` U_ n e. NN ( F ` n ) ) = ( M ` U. ran F ) )
67 eqidd 
 |-  ( ph -> NN = NN )
68 67 orcd 
 |-  ( ph -> ( NN = NN \/ NN = ( 1 ..^ ( i + 1 ) ) ) )
69 38 39 68 2 9 measiuns 
 |-  ( ph -> ( M ` U_ n e. NN ( F ` n ) ) = sum* n e. NN ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) )
70 66 69 eqtr3d 
 |-  ( ph -> ( M ` U. ran F ) = sum* n e. NN ( M ` ( ( F ` n ) \ U_ k e. ( 1 ..^ n ) ( F ` k ) ) ) )
71 33 58 70 3brtr4d 
 |-  ( ph -> ( M o. F ) ( ~~>t ` J ) ( M ` U. ran F ) )