Theorem caragenuncllem

Description: The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenuncllem.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenuncllem.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
	caragenuncllem.e	$$⊢\phi \to E\in S$$
	caragenuncllem.f	$$⊢\phi \to F\in S$$
	caragenuncllem.x	$$⊢X=\bigcup \mathrm{dom}O$$
	caragenuncllem.a	$$⊢\phi \to A\subseteq X$$
Assertion	caragenuncllem	$$⊢\phi \to O\left(A\cap \left(E\cup F\right)\right){+}_{𝑒}O\left(A\setminus \left(E\cup F\right)\right)=O\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		caragenuncllem.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenuncllem.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3		caragenuncllem.e	$$⊢\phi \to E\in S$$
4		caragenuncllem.f	$$⊢\phi \to F\in S$$
5		caragenuncllem.x	$$⊢X=\bigcup \mathrm{dom}O$$
6		caragenuncllem.a	$$⊢\phi \to A\subseteq X$$
7	6	ssinss1d	$$⊢\phi \to A\cap \left(E\cup F\right)\subseteq X$$
8	1 2 5 3 7	caragensplit	$$⊢\phi \to O\left(\left(A\cap \left(E\cup F\right)\right)\cap E\right){+}_{𝑒}O\left(\left(A\cap \left(E\cup F\right)\right)\setminus E\right)=O\left(A\cap \left(E\cup F\right)\right)$$
9	8	eqcomd	$$⊢\phi \to O\left(A\cap \left(E\cup F\right)\right)=O\left(\left(A\cap \left(E\cup F\right)\right)\cap E\right){+}_{𝑒}O\left(\left(A\cap \left(E\cup F\right)\right)\setminus E\right)$$
10		inass	$$⊢\left(A\cap \left(E\cup F\right)\right)\cap E=A\cap \left(\left(E\cup F\right)\cap E\right)$$
11		incom	$$⊢\left(E\cup F\right)\cap E=E\cap \left(E\cup F\right)$$
12		inabs	$$⊢E\cap \left(E\cup F\right)=E$$
13	11 12	eqtri	$$⊢\left(E\cup F\right)\cap E=E$$
14	13	ineq2i	$$⊢A\cap \left(\left(E\cup F\right)\cap E\right)=A\cap E$$
15	10 14	eqtri	$$⊢\left(A\cap \left(E\cup F\right)\right)\cap E=A\cap E$$
16	15	fveq2i	$$⊢O\left(\left(A\cap \left(E\cup F\right)\right)\cap E\right)=O\left(A\cap E\right)$$
17		incom	$$⊢\left(A\setminus E\right)\cap F=F\cap \left(A\setminus E\right)$$
18		indifcom	$$⊢F\cap \left(A\setminus E\right)=A\cap \left(F\setminus E\right)$$
19	17 18	eqtr2i	$$⊢A\cap \left(F\setminus E\right)=\left(A\setminus E\right)\cap F$$
20	19	eqcomi	$$⊢\left(A\setminus E\right)\cap F=A\cap \left(F\setminus E\right)$$
21		difundir	$$⊢\left(E\cup F\right)\setminus E=\left(E\setminus E\right)\cup \left(F\setminus E\right)$$
22		difid	$$⊢E\setminus E=\varnothing$$
23	22	uneq1i	$$⊢\left(E\setminus E\right)\cup \left(F\setminus E\right)=\varnothing \cup \left(F\setminus E\right)$$
24		0un	$$⊢\varnothing \cup \left(F\setminus E\right)=F\setminus E$$
25	21 23 24	3eqtrri	$$⊢F\setminus E=\left(E\cup F\right)\setminus E$$
26	25	ineq2i	$$⊢A\cap \left(F\setminus E\right)=A\cap \left(\left(E\cup F\right)\setminus E\right)$$
27		indif2	$$⊢A\cap \left(\left(E\cup F\right)\setminus E\right)=\left(A\cap \left(E\cup F\right)\right)\setminus E$$
28	20 26 27	3eqtrri	$$⊢\left(A\cap \left(E\cup F\right)\right)\setminus E=\left(A\setminus E\right)\cap F$$
29	28	fveq2i	$$⊢O\left(\left(A\cap \left(E\cup F\right)\right)\setminus E\right)=O\left(\left(A\setminus E\right)\cap F\right)$$
30	16 29	oveq12i	$$⊢O\left(\left(A\cap \left(E\cup F\right)\right)\cap E\right){+}_{𝑒}O\left(\left(A\cap \left(E\cup F\right)\right)\setminus E\right)=O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)$$
31	30	a1i	$$⊢\phi \to O\left(\left(A\cap \left(E\cup F\right)\right)\cap E\right){+}_{𝑒}O\left(\left(A\cap \left(E\cup F\right)\right)\setminus E\right)=O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)$$
32		eqidd	$$⊢\phi \to O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)=O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)$$
33	9 31 32	3eqtrd	$$⊢\phi \to O\left(A\cap \left(E\cup F\right)\right)=O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)$$
34		difun1	$$⊢A\setminus \left(E\cup F\right)=\left(A\setminus E\right)\setminus F$$
35	34	fveq2i	$$⊢O\left(A\setminus \left(E\cup F\right)\right)=O\left(\left(A\setminus E\right)\setminus F\right)$$
36	35	a1i	$$⊢\phi \to O\left(A\setminus \left(E\cup F\right)\right)=O\left(\left(A\setminus E\right)\setminus F\right)$$
37	33 36	oveq12d	$$⊢\phi \to O\left(A\cap \left(E\cup F\right)\right){+}_{𝑒}O\left(A\setminus \left(E\cup F\right)\right)=\left(O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)$$
38	6	ssinss1d	$$⊢\phi \to A\cap E\subseteq X$$
39	1 5 38	omexrcl	$$⊢\phi \to O\left(A\cap E\right)\in {ℝ}^{*}$$
40	1 5 38	omecl	$$⊢\phi \to O\left(A\cap E\right)\in \left[0,\mathrm{+\infty }\right]$$
41	40	xrge0nemnfd	$$⊢\phi \to O\left(A\cap E\right)\ne \mathrm{-\infty }$$
42	39 41	jca	$$⊢\phi \to \left(O\left(A\cap E\right)\in {ℝ}^{*}\wedge O\left(A\cap E\right)\ne \mathrm{-\infty }\right)$$
43	1 2 4 5	caragenelss	$$⊢\phi \to F\subseteq X$$
44	43	ssinss2d	$$⊢\phi \to \left(A\setminus E\right)\cap F\subseteq X$$
45	1 5 44	omexrcl	$$⊢\phi \to O\left(\left(A\setminus E\right)\cap F\right)\in {ℝ}^{*}$$
46	1 5 44	omecl	$$⊢\phi \to O\left(\left(A\setminus E\right)\cap F\right)\in \left[0,\mathrm{+\infty }\right]$$
47	46	xrge0nemnfd	$$⊢\phi \to O\left(\left(A\setminus E\right)\cap F\right)\ne \mathrm{-\infty }$$
48	45 47	jca	$$⊢\phi \to \left(O\left(\left(A\setminus E\right)\cap F\right)\in {ℝ}^{*}\wedge O\left(\left(A\setminus E\right)\cap F\right)\ne \mathrm{-\infty }\right)$$
49	6	ssdifssd	$$⊢\phi \to A\setminus E\subseteq X$$
50	49	ssdifssd	$$⊢\phi \to \left(A\setminus E\right)\setminus F\subseteq X$$
51	1 5 50	omexrcl	$$⊢\phi \to O\left(\left(A\setminus E\right)\setminus F\right)\in {ℝ}^{*}$$
52	1 5 50	omecl	$$⊢\phi \to O\left(\left(A\setminus E\right)\setminus F\right)\in \left[0,\mathrm{+\infty }\right]$$
53	52	xrge0nemnfd	$$⊢\phi \to O\left(\left(A\setminus E\right)\setminus F\right)\ne \mathrm{-\infty }$$
54	51 53	jca	$$⊢\phi \to \left(O\left(\left(A\setminus E\right)\setminus F\right)\in {ℝ}^{*}\wedge O\left(\left(A\setminus E\right)\setminus F\right)\ne \mathrm{-\infty }\right)$$
55		xaddass	$$⊢\left(\left(O\left(A\cap E\right)\in {ℝ}^{*}\wedge O\left(A\cap E\right)\ne \mathrm{-\infty }\right)\wedge \left(O\left(\left(A\setminus E\right)\cap F\right)\in {ℝ}^{*}\wedge O\left(\left(A\setminus E\right)\cap F\right)\ne \mathrm{-\infty }\right)\wedge \left(O\left(\left(A\setminus E\right)\setminus F\right)\in {ℝ}^{*}\wedge O\left(\left(A\setminus E\right)\setminus F\right)\ne \mathrm{-\infty }\right)\right)\to \left(O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)=O\left(A\cap E\right){+}_{𝑒}\left(O\left(\left(A\setminus E\right)\cap F\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)\right)$$
56	42 48 54 55	syl3anc	$$⊢\phi \to \left(O\left(A\cap E\right){+}_{𝑒}O\left(\left(A\setminus E\right)\cap F\right)\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)=O\left(A\cap E\right){+}_{𝑒}\left(O\left(\left(A\setminus E\right)\cap F\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)\right)$$
57	1 2 5 4 49	caragensplit	$$⊢\phi \to O\left(\left(A\setminus E\right)\cap F\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)=O\left(A\setminus E\right)$$
58	57	oveq2d	$$⊢\phi \to O\left(A\cap E\right){+}_{𝑒}\left(O\left(\left(A\setminus E\right)\cap F\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)\right)=O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)$$
59	1 2 5 3 6	caragensplit	$$⊢\phi \to O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)=O\left(A\right)$$
60	58 59	eqtrd	$$⊢\phi \to O\left(A\cap E\right){+}_{𝑒}\left(O\left(\left(A\setminus E\right)\cap F\right){+}_{𝑒}O\left(\left(A\setminus E\right)\setminus F\right)\right)=O\left(A\right)$$
61	37 56 60	3eqtrd	$$⊢\phi \to O\left(A\cap \left(E\cup F\right)\right){+}_{𝑒}O\left(A\setminus \left(E\cup F\right)\right)=O\left(A\right)$$