measunl

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

	Ref	Expression
Hypotheses	measunl.1	$⊢ φ \to M \in measures (S)$
	measunl.2	$⊢ φ \to A \in S$
	measunl.3	$⊢ φ \to B \in S$
Assertion	measunl	$⊢ φ \to M (A \cup B) \leq M (A) +_{𝑒} M (B)$

Proof

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

Metamath Proof Explorer

Theorem measunl

Proof