Metamath Proof Explorer

Theorem measunl

Description: A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypotheses measunl.1 ⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
measunl.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
measunl.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
Assertion measunl ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 measunl.1 ⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
2 measunl.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
3 measunl.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
4 undif1 ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
5 4 fveq2i ⊢ ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) )
6 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
7 1 6 syl ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
8 difelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 )
9 7 2 3 8 syl3anc ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 )
10 incom ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 )
11 disjdif ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
12 10 11 eqtr3i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅
13 12 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ )
14 measun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
15 1 9 3 13 14 syl121anc ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
16 5 15 syl5eqr ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
17 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
18 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
19 1 9 18 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
20 17 19 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* )
21 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
22 1 2 21 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
23 17 22 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
24 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
25 1 3 24 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
26 17 25 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
27 inelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )
28 7 2 3 27 syl3anc ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )
29 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
30 1 28 29 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
31 elxrge0 ⊢ ( ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* ∧ 0 ≤ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
32 30 31 sylib ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* ∧ 0 ≤ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
33 32 simprd ⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) )
34 17 30 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* )
35 xraddge02 ⊢ ( ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* ) → ( 0 ≤ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ≤ ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
36 20 34 35 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ≤ ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
37 33 36 mpd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ≤ ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
38 uncom ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∩ 𝐵 ) )
39 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
40 38 39 eqtr3i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = 𝐴
41 40 fveq2i ⊢ ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝑀 ‘ 𝐴 )
42 incom ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐴 ∩ 𝐵 ) )
43 inindif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
44 42 43 eqtr3i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅
45 44 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅ )
46 measun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅ ) → ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
47 1 9 28 45 46 syl121anc ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
48 41 47 syl5eqr ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
49 37 48 breqtrrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ≤ ( 𝑀 ‘ 𝐴 ) )
50 xleadd1a ⊢ ( ( ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐵 ) ∈ ℝ* ) ∧ ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ≤ ( 𝑀 ‘ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
51 20 23 26 49 50 syl31anc ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
52 16 51 eqbrtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )