Metamath Proof Explorer

Theorem measiun

Description: A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016) (Proof shortened by Thierry Arnoux, 7-Feb-2017)

Ref Expression
Hypotheses measiun.1 
|- ( ph -> M e. ( measures ` S ) )
measiun.2 
|- ( ph -> A e. S )
measiun.3 
|- ( ( ph /\ n e. NN ) -> B e. S )
measiun.4 
|- ( ph -> A C_ U_ n e. NN B )
Assertion measiun 
|- ( ph -> ( M ` A ) <_ sum* n e. NN ( M ` B ) )

Proof

Step Hyp Ref Expression
1 measiun.1 
 |-  ( ph -> M e. ( measures ` S ) )
2 measiun.2 
 |-  ( ph -> A e. S )
3 measiun.3 
 |-  ( ( ph /\ n e. NN ) -> B e. S )
4 measiun.4 
 |-  ( ph -> A C_ U_ n e. NN B )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )
7 1 2 6 syl2anc 
 |-  ( ph -> ( M ` A ) e. ( 0 [,] +oo ) )
8 5 7 sseldi 
 |-  ( ph -> ( M ` A ) e. RR* )
9 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
10 1 9 syl 
 |-  ( ph -> S e. U. ran sigAlgebra )
11 3 ralrimiva 
 |-  ( ph -> A. n e. NN B e. S )
12 sigaclcu2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. n e. NN B e. S ) -> U_ n e. NN B e. S )
13 10 11 12 syl2anc 
 |-  ( ph -> U_ n e. NN B e. S )
14 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ U_ n e. NN B e. S ) -> ( M ` U_ n e. NN B ) e. ( 0 [,] +oo ) )
15 1 13 14 syl2anc 
 |-  ( ph -> ( M ` U_ n e. NN B ) e. ( 0 [,] +oo ) )
16 5 15 sseldi 
 |-  ( ph -> ( M ` U_ n e. NN B ) e. RR* )
17 nnex 
 |-  NN e. _V
18 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> M e. ( measures ` S ) )
19 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. ( 0 [,] +oo ) )
20 18 3 19 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( M ` B ) e. ( 0 [,] +oo ) )
21 20 ralrimiva 
 |-  ( ph -> A. n e. NN ( M ` B ) e. ( 0 [,] +oo ) )
22 nfcv 
 |-  F/_ n NN
23 22 esumcl 
 |-  ( ( NN e. _V /\ A. n e. NN ( M ` B ) e. ( 0 [,] +oo ) ) -> sum* n e. NN ( M ` B ) e. ( 0 [,] +oo ) )
24 17 21 23 sylancr 
 |-  ( ph -> sum* n e. NN ( M ` B ) e. ( 0 [,] +oo ) )
25 5 24 sseldi 
 |-  ( ph -> sum* n e. NN ( M ` B ) e. RR* )
26 1 2 13 4 measssd 
 |-  ( ph -> ( M ` A ) <_ ( M ` U_ n e. NN B ) )
27 nfcsb1v 
 |-  F/_ n [_ k / n ]_ B
28 csbeq1a 
 |-  ( n = k -> B = [_ k / n ]_ B )
29 eqidd 
 |-  ( ph -> NN = NN )
30 29 orcd 
 |-  ( ph -> ( NN = NN \/ NN = ( 1 ..^ m ) ) )
31 27 28 30 1 3 measiuns 
 |-  ( ph -> ( M ` U_ n e. NN B ) = sum* n e. NN ( M ` ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) ) )
32 17 a1i 
 |-  ( ph -> NN e. _V )
33 10 adantr 
 |-  ( ( ph /\ n e. NN ) -> S e. U. ran sigAlgebra )
34 nfv 
 |-  F/ n ph
35 nfcv 
 |-  F/_ n k
36 35 nfel1 
 |-  F/ n k e. NN
37 27 nfel1 
 |-  F/ n [_ k / n ]_ B e. S
38 36 37 nfim 
 |-  F/ n ( k e. NN -> [_ k / n ]_ B e. S )
39 34 38 nfim 
 |-  F/ n ( ph -> ( k e. NN -> [_ k / n ]_ B e. S ) )
40 eleq1w 
 |-  ( n = k -> ( n e. NN <-> k e. NN ) )
41 28 eleq1d 
 |-  ( n = k -> ( B e. S <-> [_ k / n ]_ B e. S ) )
42 40 41 imbi12d 
 |-  ( n = k -> ( ( n e. NN -> B e. S ) <-> ( k e. NN -> [_ k / n ]_ B e. S ) ) )
43 42 imbi2d 
 |-  ( n = k -> ( ( ph -> ( n e. NN -> B e. S ) ) <-> ( ph -> ( k e. NN -> [_ k / n ]_ B e. S ) ) ) )
44 3 ex 
 |-  ( ph -> ( n e. NN -> B e. S ) )
45 39 43 44 chvarfv 
 |-  ( ph -> ( k e. NN -> [_ k / n ]_ B e. S ) )
46 45 ralrimiv 
 |-  ( ph -> A. k e. NN [_ k / n ]_ B e. S )
47 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
48 ssralv 
 |-  ( ( 1 ..^ n ) C_ NN -> ( A. k e. NN [_ k / n ]_ B e. S -> A. k e. ( 1 ..^ n ) [_ k / n ]_ B e. S ) )
49 47 48 ax-mp 
 |-  ( A. k e. NN [_ k / n ]_ B e. S -> A. k e. ( 1 ..^ n ) [_ k / n ]_ B e. S )
50 sigaclfu2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ n ) [_ k / n ]_ B e. S ) -> U_ k e. ( 1 ..^ n ) [_ k / n ]_ B e. S )
51 49 50 sylan2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN [_ k / n ]_ B e. S ) -> U_ k e. ( 1 ..^ n ) [_ k / n ]_ B e. S )
52 10 46 51 syl2anc 
 |-  ( ph -> U_ k e. ( 1 ..^ n ) [_ k / n ]_ B e. S )
53 52 adantr 
 |-  ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ..^ n ) [_ k / n ]_ B e. S )
54 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ B e. S /\ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B e. S ) -> ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) e. S )
55 33 3 53 54 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) e. S )
56 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) e. S ) -> ( M ` ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) ) e. ( 0 [,] +oo ) )
57 18 55 56 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) ) e. ( 0 [,] +oo ) )
58 difssd 
 |-  ( ( ph /\ n e. NN ) -> ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) C_ B )
59 18 55 3 58 measssd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) ) <_ ( M ` B ) )
60 32 57 20 59 esumle 
 |-  ( ph -> sum* n e. NN ( M ` ( B \ U_ k e. ( 1 ..^ n ) [_ k / n ]_ B ) ) <_ sum* n e. NN ( M ` B ) )
61 31 60 eqbrtrd 
 |-  ( ph -> ( M ` U_ n e. NN B ) <_ sum* n e. NN ( M ` B ) )
62 8 16 25 26 61 xrletrd 
 |-  ( ph -> ( M ` A ) <_ sum* n e. NN ( M ` B ) )