volinun

Description: Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
2	1	fveq2i	$⊢ vol ((A \cap B) \cup (A ∖ B)) = vol (A)$
3		inmbl	$⊢ (A \in dom vol \land B \in dom vol) \to A \cap B \in dom vol$
4	3	adantr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to A \cap B \in dom vol$
5		difmbl	$⊢ (A \in dom vol \land B \in dom vol) \to A ∖ B \in dom vol$
6	5	adantr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to A ∖ B \in dom vol$
7		indifcom	$⊢ (A \cap B) \cap (A ∖ B) = A \cap ((A \cap B) ∖ B)$
8		difin0	$⊢ (A \cap B) ∖ B = \emptyset$
9	8	ineq2i	$⊢ A \cap ((A \cap B) ∖ B) = A \cap \emptyset$
10		in0	$⊢ A \cap \emptyset = \emptyset$
11	9 10	eqtri	$⊢ A \cap ((A \cap B) ∖ B) = \emptyset$
12	7 11	eqtri	$⊢ (A \cap B) \cap (A ∖ B) = \emptyset$
13	12	a1i	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to (A \cap B) \cap (A ∖ B) = \emptyset$
14		mblvol	$⊢ A \cap B \in dom vol \to vol (A \cap B) = {vol}^{*} (A \cap B)$
15	4 14	syl	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cap B) = {vol}^{*} (A \cap B)$
16		inss1	$⊢ A \cap B \subseteq A$
17	16	a1i	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to A \cap B \subseteq A$
18		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
19	18	ad2antrr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to A \subseteq ℝ$
20		mblvol	$⊢ A \in dom vol \to vol (A) = {vol}^{*} (A)$
21	20	ad2antrr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A) = {vol}^{*} (A)$
22		simprl	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A) \in ℝ$
23	21 22	eqeltrrd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to {vol}^{*} (A) \in ℝ$
24		ovolsscl	$⊢ (A \cap B \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap B) \in ℝ$
25	17 19 23 24	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to {vol}^{*} (A \cap B) \in ℝ$
26	15 25	eqeltrd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cap B) \in ℝ$
27		mblvol	$⊢ A ∖ B \in dom vol \to vol (A ∖ B) = {vol}^{*} (A ∖ B)$
28	6 27	syl	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A ∖ B) = {vol}^{*} (A ∖ B)$
29		difssd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to A ∖ B \subseteq A$
30		ovolsscl	$⊢ (A ∖ B \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ B) \in ℝ$
31	29 19 23 30	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to {vol}^{*} (A ∖ B) \in ℝ$
32	28 31	eqeltrd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A ∖ B) \in ℝ$
33		volun	$⊢ ((A \cap B \in dom vol \land A ∖ B \in dom vol \land (A \cap B) \cap (A ∖ B) = \emptyset) \land (vol (A \cap B) \in ℝ \land vol (A ∖ B) \in ℝ)) \to vol ((A \cap B) \cup (A ∖ B)) = vol (A \cap B) + vol (A ∖ B)$
34	4 6 13 26 32 33	syl32anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol ((A \cap B) \cup (A ∖ B)) = vol (A \cap B) + vol (A ∖ B)$
35	2 34	syl5eqr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A) = vol (A \cap B) + vol (A ∖ B)$
36	35	oveq1d	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A) + vol (B) = vol (A \cap B) + vol (A ∖ B) + vol (B)$
37	26	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cap B) \in ℂ$
38	32	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A ∖ B) \in ℂ$
39		simprr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (B) \in ℝ$
40	39	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (B) \in ℂ$
41	37 38 40	addassd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cap B) + vol (A ∖ B) + vol (B) = vol (A \cap B) + vol (A ∖ B) + vol (B)$
42		undif1	$⊢ (A ∖ B) \cup B = A \cup B$
43	42	fveq2i	$⊢ vol ((A ∖ B) \cup B) = vol (A \cup B)$
44		simplr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to B \in dom vol$
45		incom	$⊢ (A ∖ B) \cap B = B \cap (A ∖ B)$
46		disjdif	$⊢ B \cap (A ∖ B) = \emptyset$
47	45 46	eqtri	$⊢ (A ∖ B) \cap B = \emptyset$
48	47	a1i	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to (A ∖ B) \cap B = \emptyset$
49		volun	$⊢ ((A ∖ B \in dom vol \land B \in dom vol \land (A ∖ B) \cap B = \emptyset) \land (vol (A ∖ B) \in ℝ \land vol (B) \in ℝ)) \to vol ((A ∖ B) \cup B) = vol (A ∖ B) + vol (B)$
50	6 44 48 32 39 49	syl32anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol ((A ∖ B) \cup B) = vol (A ∖ B) + vol (B)$
51	43 50	syl5reqr	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A ∖ B) + vol (B) = vol (A \cup B)$
52	51	oveq2d	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A \cap B) + vol (A ∖ B) + vol (B) = vol (A \cap B) + vol (A \cup B)$
53	36 41 52	3eqtrd	$⊢ ((A \in dom vol \land B \in dom vol) \land (vol (A) \in ℝ \land vol (B) \in ℝ)) \to vol (A) + vol (B) = vol (A \cap B) + vol (A \cup B)$

Metamath Proof Explorer

Theorem volinun

Proof