Theorem ovolsplit

Description: The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypothesis	ovolsplit.1	$$⊢\phi \to A\subseteq ℝ$$
Assertion	ovolsplit	$$⊢\phi \to {vol}^{*}\left(A\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovolsplit.1	$$⊢\phi \to A\subseteq ℝ$$
2		inundif	$$⊢\left(A\cap B\right)\cup \left(A\setminus B\right)=A$$
3	2	eqcomi	$$⊢A=\left(A\cap B\right)\cup \left(A\setminus B\right)$$
4	3	a1i	$$⊢\phi \to A=\left(A\cap B\right)\cup \left(A\setminus B\right)$$
5	4	fveq2d	$$⊢\phi \to {vol}^{*}\left(A\right)={vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)$$
6	1	ssinss1d	$$⊢\phi \to A\cap B\subseteq ℝ$$
7	1	ssdifssd	$$⊢\phi \to A\setminus B\subseteq ℝ$$
8	6 7	unssd	$$⊢\phi \to \left(A\cap B\right)\cup \left(A\setminus B\right)\subseteq ℝ$$
9		ovolcl	$$⊢\left(A\cap B\right)\cup \left(A\setminus B\right)\subseteq ℝ\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\in {ℝ}^{*}$$
10	8 9	syl	$$⊢\phi \to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\in {ℝ}^{*}$$
11		pnfge	$$⊢{vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\in {ℝ}^{*}\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le \mathrm{+\infty }$$
12	10 11	syl	$$⊢\phi \to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le \mathrm{+\infty }$$
13	12	adantr	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le \mathrm{+\infty }$$
14		oveq1	$$⊢{vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }{+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
15	14	adantl	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }{+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
16		ovolcl	$$⊢A\setminus B\subseteq ℝ\to {vol}^{*}\left(A\setminus B\right)\in {ℝ}^{*}$$
17	7 16	syl	$$⊢\phi \to {vol}^{*}\left(A\setminus B\right)\in {ℝ}^{*}$$
18	17	adantr	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\in {ℝ}^{*}$$
19		reex	$$⊢ℝ\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
21	20 1	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
22	21	difexd	$$⊢\phi \to A\setminus B\in \mathrm{V}$$
23		elpwg	$$⊢A\setminus B\in \mathrm{V}\to \left(A\setminus B\in 𝒫ℝ\leftrightarrow A\setminus B\subseteq ℝ\right)$$
24	22 23	syl	$$⊢\phi \to \left(A\setminus B\in 𝒫ℝ\leftrightarrow A\setminus B\subseteq ℝ\right)$$
25	7 24	mpbird	$$⊢\phi \to A\setminus B\in 𝒫ℝ$$
26		ovolf	$$⊢{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]$$
27	26	ffvelcdmi	$$⊢A\setminus B\in 𝒫ℝ\to {vol}^{*}\left(A\setminus B\right)\in \left[0,\mathrm{+\infty }\right]$$
28	25 27	syl	$$⊢\phi \to {vol}^{*}\left(A\setminus B\right)\in \left[0,\mathrm{+\infty }\right]$$
29	28	xrge0nemnfd	$$⊢\phi \to {vol}^{*}\left(A\setminus B\right)\ne \mathrm{-\infty }$$
30	29	adantr	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\ne \mathrm{-\infty }$$
31		xaddpnf2	$$⊢\left({vol}^{*}\left(A\setminus B\right)\in {ℝ}^{*}\wedge {vol}^{*}\left(A\setminus B\right)\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }$$
32	18 30 31	syl2anc	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }$$
33	15 32	eqtr2d	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to \mathrm{+\infty }={vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
34	13 33	breqtrd	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
35		simpl	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to \phi$$
36	20 6	sselpwd	$$⊢\phi \to A\cap B\in 𝒫ℝ$$
37	26	ffvelcdmi	$$⊢A\cap B\in 𝒫ℝ\to {vol}^{*}\left(A\cap B\right)\in \left[0,\mathrm{+\infty }\right]$$
38	36 37	syl	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)\in \left[0,\mathrm{+\infty }\right]$$
39	38	adantr	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right)\in \left[0,\mathrm{+\infty }\right]$$
40		neqne	$$⊢\neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\to {vol}^{*}\left(A\cap B\right)\ne \mathrm{+\infty }$$
41	40	adantl	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right)\ne \mathrm{+\infty }$$
42		ge0xrre	$$⊢\left({vol}^{*}\left(A\cap B\right)\in \left[0,\mathrm{+\infty }\right]\wedge {vol}^{*}\left(A\cap B\right)\ne \mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right)\in ℝ$$
43	39 41 42	syl2anc	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right)\in ℝ$$
44	12	adantr	$$⊢\left(\phi \wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le \mathrm{+\infty }$$
45		oveq2	$$⊢{vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)={vol}^{*}\left(A\cap B\right){+}_{𝑒}\mathrm{+\infty }$$
46	45	adantl	$$⊢\left(\phi \wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)={vol}^{*}\left(A\cap B\right){+}_{𝑒}\mathrm{+\infty }$$
47		ovolcl	$$⊢A\cap B\subseteq ℝ\to {vol}^{*}\left(A\cap B\right)\in {ℝ}^{*}$$
48	6 47	syl	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)\in {ℝ}^{*}$$
49	38	xrge0nemnfd	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)\ne \mathrm{-\infty }$$
50		xaddpnf1	$$⊢\left({vol}^{*}\left(A\cap B\right)\in {ℝ}^{*}\wedge {vol}^{*}\left(A\cap B\right)\ne \mathrm{-\infty }\right)\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
51	48 49 50	syl2anc	$$⊢\phi \to {vol}^{*}\left(A\cap B\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
52	51	adantr	$$⊢\left(\phi \wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
53	46 52	eqtr2d	$$⊢\left(\phi \wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to \mathrm{+\infty }={vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
54	44 53	breqtrd	$$⊢\left(\phi \wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
55	54	adantlr	$$⊢\left(\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
56		simpll	$$⊢\left(\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to \phi$$
57		simplr	$$⊢\left(\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\cap B\right)\in ℝ$$
58	28	adantr	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\in \left[0,\mathrm{+\infty }\right]$$
59		neqne	$$⊢\neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\to {vol}^{*}\left(A\setminus B\right)\ne \mathrm{+\infty }$$
60	59	adantl	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\ne \mathrm{+\infty }$$
61		ge0xrre	$$⊢\left({vol}^{*}\left(A\setminus B\right)\in \left[0,\mathrm{+\infty }\right]\wedge {vol}^{*}\left(A\setminus B\right)\ne \mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\in ℝ$$
62	58 60 61	syl2anc	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\in ℝ$$
63	62	adantlr	$$⊢\left(\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(A\setminus B\right)\in ℝ$$
64	6	3ad2ant1	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to A\cap B\subseteq ℝ$$
65		simp2	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(A\cap B\right)\in ℝ$$
66	7	3ad2ant1	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to A\setminus B\subseteq ℝ$$
67		simp3	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(A\setminus B\right)\in ℝ$$
68		ovolun	$$⊢\left(\left(A\cap B\subseteq ℝ\wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge \left(A\setminus B\subseteq ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right)+{vol}^{*}\left(A\setminus B\right)$$
69	64 65 66 67 68	syl22anc	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right)+{vol}^{*}\left(A\setminus B\right)$$
70		rexadd	$$⊢\left({vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)={vol}^{*}\left(A\cap B\right)+{vol}^{*}\left(A\setminus B\right)$$
71	70	eqcomd	$$⊢\left({vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(A\cap B\right)+{vol}^{*}\left(A\setminus B\right)={vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
72	71	3adant1	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(A\cap B\right)+{vol}^{*}\left(A\setminus B\right)={vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
73	69 72	breqtrd	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\wedge {vol}^{*}\left(A\setminus B\right)\in ℝ\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
74	56 57 63 73	syl3anc	$$⊢\left(\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\wedge \neg {vol}^{*}\left(A\setminus B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
75	55 74	pm2.61dan	$$⊢\left(\phi \wedge {vol}^{*}\left(A\cap B\right)\in ℝ\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
76	35 43 75	syl2anc	$$⊢\left(\phi \wedge \neg {vol}^{*}\left(A\cap B\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
77	34 76	pm2.61dan	$$⊢\phi \to {vol}^{*}\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$
78	5 77	eqbrtrd	$$⊢\phi \to {vol}^{*}\left(A\right)\le {vol}^{*}\left(A\cap B\right){+}_{𝑒}{vol}^{*}\left(A\setminus B\right)$$