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		incom	$⊢ B \cap (A ∖ B) = (A ∖ B) \cap B$
11		disjdif	$⊢ B \cap (A ∖ B) = \emptyset$
12	10 11	eqtr3i	$⊢ (A ∖ B) \cap B = \emptyset$
13	12	a1i	$⊢ φ \to (A ∖ B) \cap B = \emptyset$
14		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)$
15	1 9 3 13 14	syl121anc	$⊢ φ \to M ((A ∖ B) \cup B) = M (A ∖ B) +_{𝑒} M (B)$
16	5 15	syl5eqr	$⊢ φ \to M (A \cup B) = M (A ∖ B) +_{𝑒} M (B)$
17		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
18		measvxrge0	$⊢ (M \in measures (S) \land A ∖ B \in S) \to M (A ∖ B) \in [0, +∞]$
19	1 9 18	syl2anc	$⊢ φ \to M (A ∖ B) \in [0, +∞]$
20	17 19	sseldi	$⊢ φ \to M (A ∖ B) \in ℝ^{*}$
21		measvxrge0	$⊢ (M \in measures (S) \land A \in S) \to M (A) \in [0, +∞]$
22	1 2 21	syl2anc	$⊢ φ \to M (A) \in [0, +∞]$
23	17 22	sseldi	$⊢ φ \to M (A) \in ℝ^{*}$
24		measvxrge0	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in [0, +∞]$
25	1 3 24	syl2anc	$⊢ φ \to M (B) \in [0, +∞]$
26	17 25	sseldi	$⊢ φ \to M (B) \in ℝ^{*}$
27		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to A \cap B \in S$
28	7 2 3 27	syl3anc	$⊢ φ \to A \cap B \in S$
29		measvxrge0	$⊢ (M \in measures (S) \land A \cap B \in S) \to M (A \cap B) \in [0, +∞]$
30	1 28 29	syl2anc	$⊢ φ \to M (A \cap B) \in [0, +∞]$
31		elxrge0	$⊢ M (A \cap B) \in [0, +∞] \leftrightarrow (M (A \cap B) \in ℝ^{*} \land 0 \leq M (A \cap B))$
32	30 31	sylib	$⊢ φ \to (M (A \cap B) \in ℝ^{*} \land 0 \leq M (A \cap B))$
33	32	simprd	$⊢ φ \to 0 \leq M (A \cap B)$
34	17 30	sseldi	$⊢ φ \to M (A \cap B) \in ℝ^{*}$
35		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))$
36	20 34 35	syl2anc	$⊢ φ \to (0 \leq M (A \cap B) \to M (A ∖ B) \leq M (A ∖ B) +_{𝑒} M (A \cap B))$
37	33 36	mpd	$⊢ φ \to M (A ∖ B) \leq M (A ∖ B) +_{𝑒} M (A \cap B)$
38		uncom	$⊢ (A \cap B) \cup (A ∖ B) = (A ∖ B) \cup (A \cap B)$
39		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
40	38 39	eqtr3i	$⊢ (A ∖ B) \cup (A \cap B) = A$
41	40	fveq2i	$⊢ M ((A ∖ B) \cup (A \cap B)) = M (A)$
42		incom	$⊢ (A \cap B) \cap (A ∖ B) = (A ∖ B) \cap (A \cap B)$
43		inindif	$⊢ (A \cap B) \cap (A ∖ B) = \emptyset$
44	42 43	eqtr3i	$⊢ (A ∖ B) \cap (A \cap B) = \emptyset$
45	44	a1i	$⊢ φ \to (A ∖ B) \cap (A \cap B) = \emptyset$
46		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)$
47	1 9 28 45 46	syl121anc	$⊢ φ \to M ((A ∖ B) \cup (A \cap B)) = M (A ∖ B) +_{𝑒} M (A \cap B)$
48	41 47	syl5eqr	$⊢ φ \to M (A) = M (A ∖ B) +_{𝑒} M (A \cap B)$
49	37 48	breqtrrd	$⊢ φ \to M (A ∖ B) \leq M (A)$
50		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)$
51	20 23 26 49 50	syl31anc	$⊢ φ \to M (A ∖ B) +_{𝑒} M (B) \leq M (A) +_{𝑒} M (B)$
52	16 51	eqbrtrd	$⊢ φ \to M (A \cup B) \leq M (A) +_{𝑒} M (B)$

Metamath Proof Explorer

Theorem measunl

Proof