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 φ M measures S
measunl.2 φ A S
measunl.3 φ B S
Assertion measunl φ M A B M A + 𝑒 M B

Proof

Step Hyp Ref Expression
1 measunl.1 φ M measures S
2 measunl.2 φ A S
3 measunl.3 φ B S
4 undif1 A B B = A B
5 4 fveq2i M A B B = M A B
6 measbase M measures S S ran sigAlgebra
7 1 6 syl φ S ran sigAlgebra
8 difelsiga S ran sigAlgebra A S B S A B S
9 7 2 3 8 syl3anc φ A B S
10 disjdifr A B B =
11 10 a1i φ A B B =
12 measun M measures S A B S B S A B B = M A B B = M A B + 𝑒 M B
13 1 9 3 11 12 syl121anc φ M A B B = M A B + 𝑒 M B
14 5 13 eqtr3id φ M A B = M A B + 𝑒 M B
15 iccssxr 0 +∞ *
16 measvxrge0 M measures S A B S M A B 0 +∞
17 1 9 16 syl2anc φ M A B 0 +∞
18 15 17 sselid φ M A B *
19 measvxrge0 M measures S A S M A 0 +∞
20 1 2 19 syl2anc φ M A 0 +∞
21 15 20 sselid φ M A *
22 measvxrge0 M measures S B S M B 0 +∞
23 1 3 22 syl2anc φ M B 0 +∞
24 15 23 sselid φ M B *
25 inelsiga S ran sigAlgebra A S B S A B S
26 7 2 3 25 syl3anc φ A B S
27 measvxrge0 M measures S A B S M A B 0 +∞
28 1 26 27 syl2anc φ M A B 0 +∞
29 elxrge0 M A B 0 +∞ M A B * 0 M A B
30 28 29 sylib φ M A B * 0 M A B
31 30 simprd φ 0 M A B
32 15 28 sselid φ M A B *
33 xraddge02 M A B * M A B * 0 M A B M A B M A B + 𝑒 M A B
34 18 32 33 syl2anc φ 0 M A B M A B M A B + 𝑒 M A B
35 31 34 mpd φ M A B M A B + 𝑒 M A B
36 uncom A B A B = A B A B
37 inundif A B A B = A
38 36 37 eqtr3i A B A B = A
39 38 fveq2i M A B A B = M A
40 incom A B A B = A B A B
41 inindif A B A B =
42 40 41 eqtr3i A B A B =
43 42 a1i φ A B A B =
44 measun M measures S A B S A B S A B A B = M A B A B = M A B + 𝑒 M A B
45 1 9 26 43 44 syl121anc φ M A B A B = M A B + 𝑒 M A B
46 39 45 eqtr3id φ M A = M A B + 𝑒 M A B
47 35 46 breqtrrd φ M A B M A
48 xleadd1a M A B * M A * M B * M A B M A M A B + 𝑒 M B M A + 𝑒 M B
49 18 21 24 47 48 syl31anc φ M A B + 𝑒 M B M A + 𝑒 M B
50 14 49 eqbrtrd φ M A B M A + 𝑒 M B