measun

Description: The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017)

		Ref	Expression
	Assertion	measun	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (A \cup B) = M (A) +_{𝑒} M (B)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M \in measures (S)$
2		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
3	2	3ad2ant1	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to S \in ⋃ ran sigAlgebra$
4		simp2l	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to A \in S$
5		simp2r	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to B \in S$
6		unelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to A \cup B \in S$
7	3 4 5 6	syl3anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to A \cup B \in S$
8		ssun2	$⊢ B \subseteq A \cup B$
9	8	a1i	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to B \subseteq A \cup B$
10		measxun2	$⊢ (M \in measures (S) \land (A \cup B \in S \land B \in S) \land B \subseteq A \cup B) \to M (A \cup B) = M (B) +_{𝑒} M ((A \cup B) ∖ B)$
11	1 7 5 9 10	syl121anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (A \cup B) = M (B) +_{𝑒} M ((A \cup B) ∖ B)$
12		difun2	$⊢ (A \cup B) ∖ B = A ∖ B$
13		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
14		uneq1	$⊢ A \cap B = \emptyset \to (A \cap B) \cup (A ∖ B) = \emptyset \cup (A ∖ B)$
15		uncom	$⊢ \emptyset \cup (A ∖ B) = (A ∖ B) \cup \emptyset$
16		un0	$⊢ (A ∖ B) \cup \emptyset = A ∖ B$
17	15 16	eqtri	$⊢ \emptyset \cup (A ∖ B) = A ∖ B$
18	14 17	eqtrdi	$⊢ A \cap B = \emptyset \to (A \cap B) \cup (A ∖ B) = A ∖ B$
19	13 18	syl5reqr	$⊢ A \cap B = \emptyset \to A ∖ B = A$
20	12 19	syl5eq	$⊢ A \cap B = \emptyset \to (A \cup B) ∖ B = A$
21	20	fveq2d	$⊢ A \cap B = \emptyset \to M ((A \cup B) ∖ B) = M (A)$
22	21	oveq2d	$⊢ A \cap B = \emptyset \to M (B) +_{𝑒} M ((A \cup B) ∖ B) = M (B) +_{𝑒} M (A)$
23	22	3ad2ant3	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (B) +_{𝑒} M ((A \cup B) ∖ B) = M (B) +_{𝑒} M (A)$
24		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
25		measvxrge0	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in [0, +∞]$
26	24 25	sseldi	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in ℝ^{*}$
27	1 5 26	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (B) \in ℝ^{*}$
28		measvxrge0	$⊢ (M \in measures (S) \land A \in S) \to M (A) \in [0, +∞]$
29	24 28	sseldi	$⊢ (M \in measures (S) \land A \in S) \to M (A) \in ℝ^{*}$
30	1 4 29	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (A) \in ℝ^{*}$
31		xaddcom	$⊢ (M (B) \in ℝ^{} \land M (A) \in ℝ^{}) \to M (B) +_{𝑒} M (A) = M (A) +_{𝑒} M (B)$
32	27 30 31	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (B) +_{𝑒} M (A) = M (A) +_{𝑒} M (B)$
33	11 23 32	3eqtrd	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land A \cap B = \emptyset) \to M (A \cup B) = M (A) +_{𝑒} M (B)$

Metamath Proof Explorer

Theorem measun

Proof