volun

Description: The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	volun	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cup B) = vol (A) + vol (B)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to A \in dom vol$
2		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
3	1 2	syl	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to A \subseteq ℝ$
4		simpl2	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to B \in dom vol$
5		mblss	$⊢ B \in dom vol \to B \subseteq ℝ$
6	4 5	syl	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to B \subseteq ℝ$
7	3 6	unssd	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to A \cup B \subseteq ℝ$
8		readdcl	$⊢ ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
9	8	adantl	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
10		simprl	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{*} (A) \in ℝ$
11		simprr	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{*} (B) \in ℝ$
12		ovolun	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B)$
13	3 10 6 11 12	syl22anc	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B)$
14		ovollecl	$⊢ (A \cup B \subseteq ℝ \land {vol}^{} (A) + {vol}^{} (B) \in ℝ \land {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B)) \to {vol}^{} (A \cup B) \in ℝ$
15	7 9 13 14	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{*} (A \cup B) \in ℝ$
16		mblsplit	$⊢ (A \in dom vol \land A \cup B \subseteq ℝ \land {vol}^{} (A \cup B) \in ℝ) \to {vol}^{} (A \cup B) = {vol}^{} ((A \cup B) \cap A) + {vol}^{} ((A \cup B) ∖ A)$
17	1 7 15 16	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) = {vol}^{} ((A \cup B) \cap A) + {vol}^{*} ((A \cup B) ∖ A)$
18		simpl3	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to A \cap B = \emptyset$
19		indir	$⊢ (A \cup B) \cap A = (A \cap A) \cup (B \cap A)$
20		inidm	$⊢ A \cap A = A$
21		incom	$⊢ B \cap A = A \cap B$
22	20 21	uneq12i	$⊢ (A \cap A) \cup (B \cap A) = A \cup (A \cap B)$
23		unabs	$⊢ A \cup (A \cap B) = A$
24	22 23	eqtri	$⊢ (A \cap A) \cup (B \cap A) = A$
25	19 24	eqtri	$⊢ (A \cup B) \cap A = A$
26	25	a1i	$⊢ A \cap B = \emptyset \to (A \cup B) \cap A = A$
27	26	fveq2d	$⊢ A \cap B = \emptyset \to {vol}^{} ((A \cup B) \cap A) = {vol}^{} (A)$
28	21	eqeq1i	$⊢ B \cap A = \emptyset \leftrightarrow A \cap B = \emptyset$
29		disj3	$⊢ B \cap A = \emptyset \leftrightarrow B = B ∖ A$
30	28 29	sylbb1	$⊢ A \cap B = \emptyset \to B = B ∖ A$
31		uncom	$⊢ A \cup B = B \cup A$
32	31	difeq1i	$⊢ (A \cup B) ∖ A = (B \cup A) ∖ A$
33		difun2	$⊢ (B \cup A) ∖ A = B ∖ A$
34	32 33	eqtri	$⊢ (A \cup B) ∖ A = B ∖ A$
35	30 34	syl6reqr	$⊢ A \cap B = \emptyset \to (A \cup B) ∖ A = B$
36	35	fveq2d	$⊢ A \cap B = \emptyset \to {vol}^{} ((A \cup B) ∖ A) = {vol}^{} (B)$
37	27 36	oveq12d	$⊢ A \cap B = \emptyset \to {vol}^{} ((A \cup B) \cap A) + {vol}^{} ((A \cup B) ∖ A) = {vol}^{} (A) + {vol}^{} (B)$
38	18 37	syl	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} ((A \cup B) \cap A) + {vol}^{} ((A \cup B) ∖ A) = {vol}^{} (A) + {vol}^{} (B)$
39	17 38	eqtrd	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) = {vol}^{} (A) + {vol}^{*} (B)$
40	39	ex	$⊢ (A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \to (({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A \cup B) = {vol}^{} (A) + {vol}^{*} (B))$
41		mblvol	$⊢ A \in dom vol \to vol (A) = {vol}^{*} (A)$
42	41	eleq1d	$⊢ A \in dom vol \to (vol (A) \in ℝ \leftrightarrow {vol}^{*} (A) \in ℝ)$
43		mblvol	$⊢ B \in dom vol \to vol (B) = {vol}^{*} (B)$
44	43	eleq1d	$⊢ B \in dom vol \to (vol (B) \in ℝ \leftrightarrow {vol}^{*} (B) \in ℝ)$
45	42 44	bi2anan9	$⊢ (A \in dom vol \land B \in dom vol) \to ((vol (A) \in ℝ \land vol (B) \in ℝ) \leftrightarrow ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ))$
46	45	3adant3	$⊢ (A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \to ((vol (A) \in ℝ \land vol (B) \in ℝ) \leftrightarrow ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ))$
47		unmbl	$⊢ (A \in dom vol \land B \in dom vol) \to A \cup B \in dom vol$
48		mblvol	$⊢ A \cup B \in dom vol \to vol (A \cup B) = {vol}^{*} (A \cup B)$
49	47 48	syl	$⊢ (A \in dom vol \land B \in dom vol) \to vol (A \cup B) = {vol}^{*} (A \cup B)$
50	41 43	oveqan12d	$⊢ (A \in dom vol \land B \in dom vol) \to vol (A) + vol (B) = {vol}^{} (A) + {vol}^{} (B)$
51	49 50	eqeq12d	$⊢ (A \in dom vol \land B \in dom vol) \to (vol (A \cup B) = vol (A) + vol (B) \leftrightarrow {vol}^{} (A \cup B) = {vol}^{} (A) + {vol}^{*} (B))$
52	51	3adant3	$⊢ (A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \to (vol (A \cup B) = vol (A) + vol (B) \leftrightarrow {vol}^{} (A \cup B) = {vol}^{} (A) + {vol}^{*} (B))$
53	40 46 52	3imtr4d	$⊢ (A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \to ((vol (A) \in ℝ \land vol (B) \in ℝ) \to vol (A \cup B) = vol (A) + vol (B))$
54	53	imp	$⊢ ((A \in dom vol \land B \in dom vol \land A \cap B = \emptyset) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cup B) = vol (A) + vol (B)$

Metamath Proof Explorer

Theorem volun

Proof