Theorem vonvolmbllem

Description: If a subset B of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with n equal to 1 ). (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	vonvolmbllem.a	$$⊢\phi \to A\in V$$
	vonvolmbllem.b	$$⊢\phi \to B\subseteq ℝ$$
	vonvolmbllem.e	$$⊢\phi \to \forall y\in 𝒫ℝ{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap B\right){+}_{𝑒}{vol}^{*}\left(y\setminus B\right)$$
	vonvolmbllem.x	$$⊢\phi \to X\subseteq {ℝ}^{\left\{A\right\}}$$
	vonvolmbllem.y	$$⊢Y=\bigcup _{f\in X}\mathrm{ran}f$$
Assertion	vonvolmbllem	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\cap \left(B^{\left\{A\right\}}\right)\right){+}_{𝑒}\mathrm{voln*}\left(\left\{A\right\}\right)\left(X\setminus \left(B^{\left\{A\right\}}\right)\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		vonvolmbllem.a	$$⊢\phi \to A\in V$$
2		vonvolmbllem.b	$$⊢\phi \to B\subseteq ℝ$$
3		vonvolmbllem.e	$$⊢\phi \to \forall y\in 𝒫ℝ{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap B\right){+}_{𝑒}{vol}^{*}\left(y\setminus B\right)$$
4		vonvolmbllem.x	$$⊢\phi \to X\subseteq {ℝ}^{\left\{A\right\}}$$
5		vonvolmbllem.y	$$⊢Y=\bigcup _{f\in X}\mathrm{ran}f$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}fY$$
7	6 1 4 5	ssmapsn	$$⊢\phi \to X=Y^{\left\{A\right\}}$$
8	7	ineq1d	$$⊢\phi \to X\cap \left(B^{\left\{A\right\}}\right)=\left(Y^{\left\{A\right\}}\right)\cap \left(B^{\left\{A\right\}}\right)$$
9		reex	$$⊢ℝ\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
11	4	sselda	$$⊢\left(\phi \wedge f\in X\right)\to f\in \left({ℝ}^{\left\{A\right\}}\right)$$
12		elmapi	$$⊢f\in \left({ℝ}^{\left\{A\right\}}\right)\to f:\left\{A\right\}⟶ℝ$$
13	11 12	syl	$$⊢\left(\phi \wedge f\in X\right)\to f:\left\{A\right\}⟶ℝ$$
14	13	frnd	$$⊢\left(\phi \wedge f\in X\right)\to \mathrm{ran}f\subseteq ℝ$$
15	14	ralrimiva	$$⊢\phi \to \forall f\in X\mathrm{ran}f\subseteq ℝ$$
16		iunss	$$⊢\bigcup _{f\in X}\mathrm{ran}f\subseteq ℝ\leftrightarrow \forall f\in X\mathrm{ran}f\subseteq ℝ$$
17	15 16	sylibr	$$⊢\phi \to \bigcup _{f\in X}\mathrm{ran}f\subseteq ℝ$$
18	5 17	eqsstrid	$$⊢\phi \to Y\subseteq ℝ$$
19	10 18	ssexd	$$⊢\phi \to Y\in \mathrm{V}$$
20	10 2	ssexd	$$⊢\phi \to B\in \mathrm{V}$$
21		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to \left\{A\right\}\in \mathrm{V}$$
23	19 20 22	inmap	$$⊢\phi \to \left(Y^{\left\{A\right\}}\right)\cap \left(B^{\left\{A\right\}}\right)={\left(Y\cap B\right)}^{\left\{A\right\}}$$
24	8 23	eqtrd	$$⊢\phi \to X\cap \left(B^{\left\{A\right\}}\right)={\left(Y\cap B\right)}^{\left\{A\right\}}$$
25	24	fveq2d	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\cap \left(B^{\left\{A\right\}}\right)\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left({\left(Y\cap B\right)}^{\left\{A\right\}}\right)$$
26	18	ssinss1d	$$⊢\phi \to Y\cap B\subseteq ℝ$$
27	1 26	ovnovol	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left({\left(Y\cap B\right)}^{\left\{A\right\}}\right)={vol}^{*}\left(Y\cap B\right)$$
28	25 27	eqtrd	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\cap \left(B^{\left\{A\right\}}\right)\right)={vol}^{*}\left(Y\cap B\right)$$
29	7	difeq1d	$$⊢\phi \to X\setminus \left(B^{\left\{A\right\}}\right)=\left(Y^{\left\{A\right\}}\right)\setminus \left(B^{\left\{A\right\}}\right)$$
30	19 20 1	difmapsn	$$⊢\phi \to \left(Y^{\left\{A\right\}}\right)\setminus \left(B^{\left\{A\right\}}\right)={\left(Y\setminus B\right)}^{\left\{A\right\}}$$
31	29 30	eqtrd	$$⊢\phi \to X\setminus \left(B^{\left\{A\right\}}\right)={\left(Y\setminus B\right)}^{\left\{A\right\}}$$
32	31	fveq2d	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\setminus \left(B^{\left\{A\right\}}\right)\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left({\left(Y\setminus B\right)}^{\left\{A\right\}}\right)$$
33	18	ssdifssd	$$⊢\phi \to Y\setminus B\subseteq ℝ$$
34	1 33	ovnovol	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left({\left(Y\setminus B\right)}^{\left\{A\right\}}\right)={vol}^{*}\left(Y\setminus B\right)$$
35	32 34	eqtrd	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\setminus \left(B^{\left\{A\right\}}\right)\right)={vol}^{*}\left(Y\setminus B\right)$$
36	28 35	oveq12d	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\cap \left(B^{\left\{A\right\}}\right)\right){+}_{𝑒}\mathrm{voln*}\left(\left\{A\right\}\right)\left(X\setminus \left(B^{\left\{A\right\}}\right)\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)$$
37	7	fveq2d	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left(Y^{\left\{A\right\}}\right)$$
38	1 18	ovnovol	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(Y^{\left\{A\right\}}\right)={vol}^{*}\left(Y\right)$$
39	19 18	elpwd	$$⊢\phi \to Y\in 𝒫ℝ$$
40		fveq2	$$⊢y=Y\to {vol}^{*}\left(y\right)={vol}^{*}\left(Y\right)$$
41		ineq1	$$⊢y=Y\to y\cap B=Y\cap B$$
42	41	fveq2d	$$⊢y=Y\to {vol}^{*}\left(y\cap B\right)={vol}^{*}\left(Y\cap B\right)$$
43		difeq1	$$⊢y=Y\to y\setminus B=Y\setminus B$$
44	43	fveq2d	$$⊢y=Y\to {vol}^{*}\left(y\setminus B\right)={vol}^{*}\left(Y\setminus B\right)$$
45	42 44	oveq12d	$$⊢y=Y\to {vol}^{*}\left(y\cap B\right){+}_{𝑒}{vol}^{*}\left(y\setminus B\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)$$
46	40 45	eqeq12d	$$⊢y=Y\to \left({vol}^{*}\left(y\right)={vol}^{*}\left(y\cap B\right){+}_{𝑒}{vol}^{*}\left(y\setminus B\right)\leftrightarrow {vol}^{*}\left(Y\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)\right)$$
47	46	rspcva	$$⊢\left(Y\in 𝒫ℝ\wedge \forall y\in 𝒫ℝ{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap B\right){+}_{𝑒}{vol}^{*}\left(y\setminus B\right)\right)\to {vol}^{*}\left(Y\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)$$
48	39 3 47	syl2anc	$$⊢\phi \to {vol}^{*}\left(Y\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)$$
49	37 38 48	3eqtrd	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\right)={vol}^{*}\left(Y\cap B\right){+}_{𝑒}{vol}^{*}\left(Y\setminus B\right)$$
50	36 49	eqtr4d	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(X\cap \left(B^{\left\{A\right\}}\right)\right){+}_{𝑒}\mathrm{voln*}\left(\left\{A\right\}\right)\left(X\setminus \left(B^{\left\{A\right\}}\right)\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left(X\right)$$