Metamath Proof Explorer

Theorem measssd

Description: A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016)

Ref Expression
Hypotheses measssd.1 
|- ( ph -> M e. ( measures ` S ) )
measssd.2 
|- ( ph -> A e. S )
measssd.3 
|- ( ph -> B e. S )
measssd.4 
|- ( ph -> A C_ B )
Assertion measssd 
|- ( ph -> ( M ` A ) <_ ( M ` B ) )

Proof

Step Hyp Ref Expression
1 measssd.1 
 |-  ( ph -> M e. ( measures ` S ) )
2 measssd.2 
 |-  ( ph -> A e. S )
3 measssd.3 
 |-  ( ph -> B e. S )
4 measssd.4 
 |-  ( ph -> A C_ B )
5 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
6 1 5 syl 
 |-  ( ph -> S e. U. ran sigAlgebra )
7 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ B e. S /\ A e. S ) -> ( B \ A ) e. S )
8 6 3 2 7 syl3anc 
 |-  ( ph -> ( B \ A ) e. S )
9 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( B \ A ) e. S ) -> ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) )
10 1 8 9 syl2anc 
 |-  ( ph -> ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) )
11 elxrge0 
 |-  ( ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) <-> ( ( M ` ( B \ A ) ) e. RR* /\ 0 <_ ( M ` ( B \ A ) ) ) )
12 11 simprbi 
 |-  ( ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) -> 0 <_ ( M ` ( B \ A ) ) )
13 10 12 syl 
 |-  ( ph -> 0 <_ ( M ` ( B \ A ) ) )
14 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )
15 1 2 14 syl2anc 
 |-  ( ph -> ( M ` A ) e. ( 0 [,] +oo ) )
16 elxrge0 
 |-  ( ( M ` A ) e. ( 0 [,] +oo ) <-> ( ( M ` A ) e. RR* /\ 0 <_ ( M ` A ) ) )
17 16 simplbi 
 |-  ( ( M ` A ) e. ( 0 [,] +oo ) -> ( M ` A ) e. RR* )
18 15 17 syl 
 |-  ( ph -> ( M ` A ) e. RR* )
19 11 simplbi 
 |-  ( ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) -> ( M ` ( B \ A ) ) e. RR* )
20 10 19 syl 
 |-  ( ph -> ( M ` ( B \ A ) ) e. RR* )
21 xraddge02 
 |-  ( ( ( M ` A ) e. RR* /\ ( M ` ( B \ A ) ) e. RR* ) -> ( 0 <_ ( M ` ( B \ A ) ) -> ( M ` A ) <_ ( ( M ` A ) +e ( M ` ( B \ A ) ) ) ) )
22 18 20 21 syl2anc 
 |-  ( ph -> ( 0 <_ ( M ` ( B \ A ) ) -> ( M ` A ) <_ ( ( M ` A ) +e ( M ` ( B \ A ) ) ) ) )
23 13 22 mpd 
 |-  ( ph -> ( M ` A ) <_ ( ( M ` A ) +e ( M ` ( B \ A ) ) ) )
24 prssi 
 |-  ( ( A e. S /\ ( B \ A ) e. S ) -> { A , ( B \ A ) } C_ S )
25 2 8 24 syl2anc 
 |-  ( ph -> { A , ( B \ A ) } C_ S )
26 prex 
 |-  { A , ( B \ A ) } e. _V
27 26 elpw 
 |-  ( { A , ( B \ A ) } e. ~P S <-> { A , ( B \ A ) } C_ S )
28 25 27 sylibr 
 |-  ( ph -> { A , ( B \ A ) } e. ~P S )
29 prct 
 |-  ( ( A e. S /\ ( B \ A ) e. S ) -> { A , ( B \ A ) } ~<_ _om )
30 2 8 29 syl2anc 
 |-  ( ph -> { A , ( B \ A ) } ~<_ _om )
31 disjdifprg 
 |-  ( ( A e. S /\ B e. S ) -> Disj_ y e. { ( B \ A ) , A } y )
32 2 3 31 syl2anc 
 |-  ( ph -> Disj_ y e. { ( B \ A ) , A } y )
33 prcom 
 |-  { ( B \ A ) , A } = { A , ( B \ A ) }
34 33 a1i 
 |-  ( ph -> { ( B \ A ) , A } = { A , ( B \ A ) } )
35 34 disjeq1d 
 |-  ( ph -> ( Disj_ y e. { ( B \ A ) , A } y <-> Disj_ y e. { A , ( B \ A ) } y ) )
36 32 35 mpbid 
 |-  ( ph -> Disj_ y e. { A , ( B \ A ) } y )
37 measvun 
 |-  ( ( M e. ( measures ` S ) /\ { A , ( B \ A ) } e. ~P S /\ ( { A , ( B \ A ) } ~<_ _om /\ Disj_ y e. { A , ( B \ A ) } y ) ) -> ( M ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( M ` y ) )
38 1 28 30 36 37 syl112anc 
 |-  ( ph -> ( M ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( M ` y ) )
39 uniprg 
 |-  ( ( A e. S /\ ( B \ A ) e. S ) -> U. { A , ( B \ A ) } = ( A u. ( B \ A ) ) )
40 2 8 39 syl2anc 
 |-  ( ph -> U. { A , ( B \ A ) } = ( A u. ( B \ A ) ) )
41 undif 
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )
42 4 41 sylib 
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
43 40 42 eqtrd 
 |-  ( ph -> U. { A , ( B \ A ) } = B )
44 43 fveq2d 
 |-  ( ph -> ( M ` U. { A , ( B \ A ) } ) = ( M ` B ) )
45 fveq2 
 |-  ( y = A -> ( M ` y ) = ( M ` A ) )
46 45 adantl 
 |-  ( ( ph /\ y = A ) -> ( M ` y ) = ( M ` A ) )
47 fveq2 
 |-  ( y = ( B \ A ) -> ( M ` y ) = ( M ` ( B \ A ) ) )
48 47 adantl 
 |-  ( ( ph /\ y = ( B \ A ) ) -> ( M ` y ) = ( M ` ( B \ A ) ) )
49 eqimss 
 |-  ( A = ( B \ A ) -> A C_ ( B \ A ) )
50 ssdifeq0 
 |-  ( A C_ ( B \ A ) <-> A = (/) )
51 49 50 sylib 
 |-  ( A = ( B \ A ) -> A = (/) )
52 51 adantl 
 |-  ( ( ph /\ A = ( B \ A ) ) -> A = (/) )
53 52 fveq2d 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( M ` A ) = ( M ` (/) ) )
54 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
55 1 54 syl 
 |-  ( ph -> ( M ` (/) ) = 0 )
56 55 adantr 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( M ` (/) ) = 0 )
57 53 56 eqtrd 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( M ` A ) = 0 )
58 57 orcd 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( ( M ` A ) = 0 \/ ( M ` A ) = +oo ) )
59 58 ex 
 |-  ( ph -> ( A = ( B \ A ) -> ( ( M ` A ) = 0 \/ ( M ` A ) = +oo ) ) )
60 46 48 2 8 15 10 59 esumpr2 
 |-  ( ph -> sum* y e. { A , ( B \ A ) } ( M ` y ) = ( ( M ` A ) +e ( M ` ( B \ A ) ) ) )
61 38 44 60 3eqtr3d 
 |-  ( ph -> ( M ` B ) = ( ( M ` A ) +e ( M ` ( B \ A ) ) ) )
62 23 61 breqtrrd 
 |-  ( ph -> ( M ` A ) <_ ( M ` B ) )