Theorem caragensplit

Description: If E is in the set generated by the Caratheodory's method, then it splits any set A in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set A . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		caragensplit.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragensplit.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3		caragensplit.x	$$⊢X=\bigcup \mathrm{dom}O$$
4		caragensplit.e	$$⊢\phi \to E\in S$$
5		caragensplit.a	$$⊢\phi \to A\subseteq X$$
6	1 3	unidmex	$$⊢\phi \to X\in \mathrm{V}$$
7		ssexg	$$⊢\left(A\subseteq X\wedge X\in \mathrm{V}\right)\to A\in \mathrm{V}$$
8	5 6 7	syl2anc	$$⊢\phi \to A\in \mathrm{V}$$
9		elpwg	$$⊢A\in \mathrm{V}\to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
10	8 9	syl	$$⊢\phi \to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
11	5 10	mpbird	$$⊢\phi \to A\in 𝒫X$$
12	3	pweqi	$$⊢𝒫X=𝒫\bigcup \mathrm{dom}O$$
13	11 12	eleqtrdi	$$⊢\phi \to A\in 𝒫\bigcup \mathrm{dom}O$$
14	1 2	caragenel	$$⊢\phi \to \left(E\in S\leftrightarrow \left(E\in 𝒫\bigcup \mathrm{dom}O\wedge \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)\right)$$
15	4 14	mpbid	$$⊢\phi \to \left(E\in 𝒫\bigcup \mathrm{dom}O\wedge \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)$$
16	15	simprd	$$⊢\phi \to \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
17		ineq1	$$⊢a=A\to a\cap E=A\cap E$$
18	17	fveq2d	$$⊢a=A\to O\left(a\cap E\right)=O\left(A\cap E\right)$$
19		difeq1	$$⊢a=A\to a\setminus E=A\setminus E$$
20	19	fveq2d	$$⊢a=A\to O\left(a\setminus E\right)=O\left(A\setminus E\right)$$
21	18 20	oveq12d	$$⊢a=A\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)$$
22		fveq2	$$⊢a=A\to O\left(a\right)=O\left(A\right)$$
23	21 22	eqeq12d	$$⊢a=A\to \left(O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\leftrightarrow O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)=O\left(A\right)\right)$$
24	23	rspcva	$$⊢\left(A\in 𝒫\bigcup \mathrm{dom}O\wedge \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)\to O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)=O\left(A\right)$$
25	13 16 24	syl2anc	$$⊢\phi \to O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)=O\left(A\right)$$