ovolunnul

Description: Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015)

		Ref	Expression
	Assertion	ovolunnul	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A \cup B) = {vol}^{*} (A)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{*} (B) = 0) \to A \subseteq ℝ$
2		simp2	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{*} (B) = 0) \to B \subseteq ℝ$
3	1 2	unssd	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{*} (B) = 0) \to A \cup B \subseteq ℝ$
4		ovolcl	$⊢ A \cup B \subseteq ℝ \to {vol}^{} (A \cup B) \in ℝ^{}$
5	3 4	syl	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A \cup B) \in ℝ^{*}$
6		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
7	6	3ad2ant1	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A) \in ℝ^{*}$
8		xrltnle	$⊢ ({vol}^{} (A) \in ℝ^{} \land {vol}^{} (A \cup B) \in ℝ^{}) \to ({vol}^{} (A) < {vol}^{} (A \cup B) \leftrightarrow \neg {vol}^{} (A \cup B) \leq {vol}^{} (A))$
9	7 5 8	syl2anc	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to ({vol}^{} (A) < {vol}^{} (A \cup B) \leftrightarrow \neg {vol}^{} (A \cup B) \leq {vol}^{*} (A))$
10	1	adantr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{*} (A \cup B)) \to A \subseteq ℝ$
11		mnfxr	$⊢ −∞ \in ℝ^{*}$
12	11	a1i	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to −∞ \in ℝ^{}$
13	10 6	syl	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) \in ℝ^{*}$
14	5	adantr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A \cup B) \in ℝ^{*}$
15		ovolge0	$⊢ A \subseteq ℝ \to 0 \leq {vol}^{*} (A)$
16	15	3ad2ant1	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to 0 \leq {vol}^{} (A)$
17		ge0gtmnf	$⊢ ({vol}^{} (A) \in ℝ^{} \land 0 \leq {vol}^{} (A)) \to −∞ < {vol}^{} (A)$
18	7 16 17	syl2anc	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to −∞ < {vol}^{} (A)$
19	18	adantr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to −∞ < {vol}^{} (A)$
20		simpr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) < {vol}^{*} (A \cup B)$
21		xrre2	$⊢ ((−∞ \in ℝ^{} \land {vol}^{} (A) \in ℝ^{} \land {vol}^{} (A \cup B) \in ℝ^{}) \land (−∞ < {vol}^{} (A) \land {vol}^{} (A) < {vol}^{} (A \cup B))) \to {vol}^{*} (A) \in ℝ$
22	12 13 14 19 20 21	syl32anc	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) \in ℝ$
23	2	adantr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{*} (A \cup B)) \to B \subseteq ℝ$
24		simpl3	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (B) = 0$
25		0re	$⊢ 0 \in ℝ$
26	24 25	eqeltrdi	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (B) \in ℝ$
27		ovolun	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B)$
28	10 22 23 26 27	syl22anc	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B)$
29	24	oveq2d	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) + {vol}^{} (B) = {vol}^{} (A) + 0$
30	22	recnd	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) \in ℂ$
31	30	addridd	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) + 0 = {vol}^{*} (A)$
32	29 31	eqtrd	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A) + {vol}^{} (B) = {vol}^{} (A)$
33	28 32	breqtrd	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \land {vol}^{} (A) < {vol}^{} (A \cup B)) \to {vol}^{} (A \cup B) \leq {vol}^{*} (A)$
34	33	ex	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to ({vol}^{} (A) < {vol}^{} (A \cup B) \to {vol}^{} (A \cup B) \leq {vol}^{*} (A))$
35	9 34	sylbird	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to (\neg {vol}^{} (A \cup B) \leq {vol}^{} (A) \to {vol}^{} (A \cup B) \leq {vol}^{*} (A))$
36	35	pm2.18d	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A \cup B) \leq {vol}^{*} (A)$
37		ssun1	$⊢ A \subseteq A \cup B$
38		ovolss	$⊢ (A \subseteq A \cup B \land A \cup B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (A \cup B)$
39	37 3 38	sylancr	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A) \leq {vol}^{*} (A \cup B)$
40	5 7 36 39	xrletrid	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land {vol}^{} (B) = 0) \to {vol}^{} (A \cup B) = {vol}^{*} (A)$

Metamath Proof Explorer

Theorem ovolunnul

Proof