measxun2

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

		Ref	Expression
	Assertion	measxun2	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (A) = M (B) +_{𝑒} M (A ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M \in measures (S)$
2		simp2r	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to B \in S$
3		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
4	1 3	syl	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to S \in ⋃ ran sigAlgebra$
5		simp2l	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to A \in S$
6		difelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to A ∖ B \in S$
7	4 5 2 6	syl3anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to A ∖ B \in S$
8		prelpwi	$⊢ (B \in S \land A ∖ B \in S) \to \{B, A ∖ B\} \in 𝒫 S$
9	2 7 8	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to \{B, A ∖ B\} \in 𝒫 S$
10		prct	$⊢ (B \in S \land A ∖ B \in S) \to \{B, A ∖ B\} ≼ ω$
11	2 7 10	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to \{B, A ∖ B\} ≼ ω$
12		simp3	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to B \subseteq A$
13		disjdifprg2	$⊢ A \in S \to \underset{x \in \{A ∖ B, A \cap B\}}{Disj} x$
14		prcom	$⊢ \{A ∖ B, B\} = \{B, A ∖ B\}$
15		dfss	$⊢ B \subseteq A \leftrightarrow B = B \cap A$
16	15	biimpi	$⊢ B \subseteq A \to B = B \cap A$
17		incom	$⊢ B \cap A = A \cap B$
18	16 17	eqtrdi	$⊢ B \subseteq A \to B = A \cap B$
19	18	preq2d	$⊢ B \subseteq A \to \{A ∖ B, B\} = \{A ∖ B, A \cap B\}$
20	14 19	eqtr3id	$⊢ B \subseteq A \to \{B, A ∖ B\} = \{A ∖ B, A \cap B\}$
21	20	disjeq1d	$⊢ B \subseteq A \to (\underset{x \in \{B, A ∖ B\}}{Disj} x \leftrightarrow \underset{x \in \{A ∖ B, A \cap B\}}{Disj} x)$
22	21	biimprd	$⊢ B \subseteq A \to (\underset{x \in \{A ∖ B, A \cap B\}}{Disj} x \to \underset{x \in \{B, A ∖ B\}}{Disj} x)$
23	13 22	mpan9	$⊢ (A \in S \land B \subseteq A) \to \underset{x \in \{B, A ∖ B\}}{Disj} x$
24	5 12 23	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to \underset{x \in \{B, A ∖ B\}}{Disj} x$
25	11 24	jca	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to (\{B, A ∖ B\} ≼ ω \land \underset{x \in \{B, A ∖ B\}}{Disj} x)$
26		measvun	$⊢ (M \in measures (S) \land \{B, A ∖ B\} \in 𝒫 S \land (\{B, A ∖ B\} ≼ ω \land \underset{x \in \{B, A ∖ B\}}{Disj} x)) \to M (⋃ \{B, A ∖ B\}) = \underset{x \in \{B, A ∖ B\}}{\sum^{*}} M (x)$
27	1 9 25 26	syl3anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (⋃ \{B, A ∖ B\}) = \underset{x \in \{B, A ∖ B\}}{\sum^{*}} M (x)$
28	2 7	jca	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to (B \in S \land A ∖ B \in S)$
29		uniprg	$⊢ (B \in S \land A ∖ B \in S) \to ⋃ \{B, A ∖ B\} = B \cup (A ∖ B)$
30		undif	$⊢ B \subseteq A \leftrightarrow B \cup (A ∖ B) = A$
31	30	biimpi	$⊢ B \subseteq A \to B \cup (A ∖ B) = A$
32	29 31	sylan9eq	$⊢ ((B \in S \land A ∖ B \in S) \land B \subseteq A) \to ⋃ \{B, A ∖ B\} = A$
33	32	fveq2d	$⊢ ((B \in S \land A ∖ B \in S) \land B \subseteq A) \to M (⋃ \{B, A ∖ B\}) = M (A)$
34	28 12 33	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (⋃ \{B, A ∖ B\}) = M (A)$
35		simpr	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land x = B) \to x = B$
36	35	fveq2d	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land x = B) \to M (x) = M (B)$
37		simpr	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land x = A ∖ B) \to x = A ∖ B$
38	37	fveq2d	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land x = A ∖ B) \to M (x) = M (A ∖ B)$
39		measvxrge0	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in [0, +∞]$
40	1 2 39	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (B) \in [0, +∞]$
41		measvxrge0	$⊢ (M \in measures (S) \land A ∖ B \in S) \to M (A ∖ B) \in [0, +∞]$
42	1 7 41	syl2anc	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (A ∖ B) \in [0, +∞]$
43		eqimss	$⊢ B = A ∖ B \to B \subseteq A ∖ B$
44		ssdifeq0	$⊢ B \subseteq A ∖ B \leftrightarrow B = \emptyset$
45	43 44	sylib	$⊢ B = A ∖ B \to B = \emptyset$
46	45	fveq2d	$⊢ B = A ∖ B \to M (B) = M (\emptyset)$
47		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
48	46 47	sylan9eqr	$⊢ (M \in measures (S) \land B = A ∖ B) \to M (B) = 0$
49	1 48	sylan	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land B = A ∖ B) \to M (B) = 0$
50	49	orcd	$⊢ ((M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \land B = A ∖ B) \to (M (B) = 0 \lor M (B) = +∞)$
51	50	ex	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to (B = A ∖ B \to (M (B) = 0 \lor M (B) = +∞))$
52	36 38 2 7 40 42 51	esumpr2	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to \underset{x \in \{B, A ∖ B\}}{\sum^{*}} M (x) = M (B) +_{𝑒} M (A ∖ B)$
53	27 34 52	3eqtr3d	$⊢ (M \in measures (S) \land (A \in S \land B \in S) \land B \subseteq A) \to M (A) = M (B) +_{𝑒} M (A ∖ B)$

Metamath Proof Explorer

Theorem measxun2

Proof