vonvolmbl

Description: A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	vonvolmbl.a	$⊢ φ \to A \in V$
	vonvolmbl.b	$⊢ φ \to B \subseteq ℝ$
Assertion	vonvolmbl	$⊢ φ \to (B^{\{A\}} \in dom voln (\{A\}) \leftrightarrow B \in dom vol)$

Proof

Step	Hyp	Ref	Expression
1		vonvolmbl.a	$⊢ φ \to A \in V$
2		vonvolmbl.b	$⊢ φ \to B \subseteq ℝ$
3		vex	$⊢ y \in V$
4	3	a1i	$⊢ φ \to y \in V$
5		reex	$⊢ ℝ \in V$
6	5	a1i	$⊢ φ \to ℝ \in V$
7	6 2	ssexd	$⊢ φ \to B \in V$
8		snfi	$⊢ \{A\} \in Fin$
9	8	a1i	$⊢ φ \to \{A\} \in Fin$
10	9	elexd	$⊢ φ \to \{A\} \in V$
11	4 7 10	inmap	$⊢ φ \to (y^{\{A\}}) \cap (B^{\{A\}}) = {(y \cap B)}^{\{A\}}$
12	11	eqcomd	$⊢ φ \to {(y \cap B)}^{\{A\}} = (y^{\{A\}}) \cap (B^{\{A\}})$
13	12	fveq2d	$⊢ φ \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) = voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}}))$
14	4 7 1	difmapsn	$⊢ φ \to (y^{\{A\}}) ∖ (B^{\{A\}}) = {(y ∖ B)}^{\{A\}}$
15	14	eqcomd	$⊢ φ \to {(y ∖ B)}^{\{A\}} = (y^{\{A\}}) ∖ (B^{\{A\}})$
16	15	fveq2d	$⊢ φ \to voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}}))$
17	13 16	oveq12d	$⊢ φ \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}}))$
18	17	ad2antrr	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}}))$
19		ovexd	$⊢ y \in 𝒫 ℝ \to y^{\{A\}} \in V$
20	5	a1i	$⊢ y \in 𝒫 ℝ \to ℝ \in V$
21		elpwi	$⊢ y \in 𝒫 ℝ \to y \subseteq ℝ$
22		mapss	$⊢ (ℝ \in V \land y \subseteq ℝ) \to y^{\{A\}} \subseteq ℝ^{\{A\}}$
23	20 21 22	syl2anc	$⊢ y \in 𝒫 ℝ \to y^{\{A\}} \subseteq ℝ^{\{A\}}$
24	19 23	elpwd	$⊢ y \in 𝒫 ℝ \to y^{\{A\}} \in 𝒫 (ℝ^{\{A\}})$
25	24	adantl	$⊢ (\forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \land y \in 𝒫 ℝ) \to y^{\{A\}} \in 𝒫 (ℝ^{\{A\}})$
26		simpl	$⊢ (\forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \land y \in 𝒫 ℝ) \to \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)$
27		ineq1	$⊢ x = y^{\{A\}} \to x \cap (B^{\{A\}}) = (y^{\{A\}}) \cap (B^{\{A\}})$
28	27	fveq2d	$⊢ x = y^{\{A\}} \to voln* (\{A\}) (x \cap (B^{\{A\}})) = voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}}))$
29		difeq1	$⊢ x = y^{\{A\}} \to x ∖ (B^{\{A\}}) = (y^{\{A\}}) ∖ (B^{\{A\}})$
30	29	fveq2d	$⊢ x = y^{\{A\}} \to voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}}))$
31	28 30	oveq12d	$⊢ x = y^{\{A\}} \to voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}}))$
32		fveq2	$⊢ x = y^{\{A\}} \to voln* (\{A\}) (x) = voln* (\{A\}) (y^{\{A\}})$
33	31 32	eqeq12d	$⊢ x = y^{\{A\}} \to (voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \leftrightarrow voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}})) = voln* (\{A\}) (y^{\{A\}}))$
34	33	rspcva	$⊢ (y^{\{A\}} \in 𝒫 (ℝ^{\{A\}}) \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \to voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}})) = voln* (\{A\}) (y^{\{A\}})$
35	25 26 34	syl2anc	$⊢ (\forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \land y \in 𝒫 ℝ) \to voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}})) = voln* (\{A\}) (y^{\{A\}})$
36	35	adantll	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) ((y^{\{A\}}) \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) ((y^{\{A\}}) ∖ (B^{\{A\}})) = voln* (\{A\}) (y^{\{A\}})$
37		eqidd	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) (y^{\{A\}}) = voln* (\{A\}) (y^{\{A\}})$
38	18 36 37	3eqtrd	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = voln* (\{A\}) (y^{\{A\}})$
39	38	eqcomd	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) (y^{\{A\}}) = voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}})$
40	1	adantr	$⊢ (φ \land y \in 𝒫 ℝ) \to A \in V$
41	21	adantl	$⊢ (φ \land y \in 𝒫 ℝ) \to y \subseteq ℝ$
42	40 41	ovnovol	$⊢ (φ \land y \in 𝒫 ℝ) \to voln* (\{A\}) (y^{\{A\}}) = {vol}^{*} (y)$
43	42	adantlr	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) (y^{\{A\}}) = {vol}^{*} (y)$
44	41	ssinss1d	$⊢ (φ \land y \in 𝒫 ℝ) \to y \cap B \subseteq ℝ$
45	40 44	ovnovol	$⊢ (φ \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) = {vol}^{*} (y \cap B)$
46	41	ssdifssd	$⊢ (φ \land y \in 𝒫 ℝ) \to y ∖ B \subseteq ℝ$
47	40 46	ovnovol	$⊢ (φ \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = {vol}^{*} (y ∖ B)$
48	45 47	oveq12d	$⊢ (φ \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)$
49	48	adantlr	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to voln* (\{A\}) ({(y \cap B)}^{\{A\}}) +_{𝑒} voln* (\{A\}) ({(y ∖ B)}^{\{A\}}) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)$
50	39 43 49	3eqtr3d	$⊢ ((φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \land y \in 𝒫 ℝ) \to {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)$
51	50	ralrimiva	$⊢ (φ \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)) \to \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)$
52	51	ex	$⊢ φ \to (\forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \to \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B))$
53	1	ad2antrr	$⊢ ((φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)) \land x \in 𝒫 (ℝ^{\{A\}})) \to A \in V$
54	2	ad2antrr	$⊢ ((φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)) \land x \in 𝒫 (ℝ^{\{A\}})) \to B \subseteq ℝ$
55		simplr	$⊢ ((φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)) \land x \in 𝒫 (ℝ^{\{A\}})) \to \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)$
56		elpwi	$⊢ x \in 𝒫 (ℝ^{\{A\}}) \to x \subseteq ℝ^{\{A\}}$
57	56	adantl	$⊢ ((φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)) \land x \in 𝒫 (ℝ^{\{A\}})) \to x \subseteq ℝ^{\{A\}}$
58		rneq	$⊢ g = f \to ran g = ran f$
59	58	cbviunv	$⊢ ⋃_{g \in x} ran g = ⋃_{f \in x} ran f$
60	53 54 55 57 59	vonvolmbllem	$⊢ ((φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)) \land x \in 𝒫 (ℝ^{\{A\}})) \to voln (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)$
61	60	ralrimiva	$⊢ (φ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B)) \to \forall x \in 𝒫 (ℝ^{\{A\}}) voln (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)$
62	61	ex	$⊢ φ \to (\forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{} (y ∖ B) \to \forall x \in 𝒫 (ℝ^{\{A\}}) voln (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x))$
63	52 62	impbid	$⊢ φ \to (\forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x) \leftrightarrow \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B))$
64		mapss	$⊢ (ℝ \in V \land B \subseteq ℝ) \to B^{\{A\}} \subseteq ℝ^{\{A\}}$
65	6 2 64	syl2anc	$⊢ φ \to B^{\{A\}} \subseteq ℝ^{\{A\}}$
66	9	isvonmbl	$⊢ φ \to (B^{\{A\}} \in dom voln (\{A\}) \leftrightarrow (B^{\{A\}} \subseteq ℝ^{\{A\}} \land \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x)))$
67	65 66	mpbirand	$⊢ φ \to (B^{\{A\}} \in dom voln (\{A\}) \leftrightarrow \forall x \in 𝒫 (ℝ^{\{A\}}) voln* (\{A\}) (x \cap (B^{\{A\}})) +_{𝑒} voln* (\{A\}) (x ∖ (B^{\{A\}})) = voln* (\{A\}) (x))$
68		ismbl4	$⊢ B \in dom vol \leftrightarrow (B \subseteq ℝ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B))$
69	68	a1i	$⊢ φ \to (B \in dom vol \leftrightarrow (B \subseteq ℝ \land \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B)))$
70	2 69	mpbirand	$⊢ φ \to (B \in dom vol \leftrightarrow \forall y \in 𝒫 ℝ {vol}^{} (y) = {vol}^{} (y \cap B) +_{𝑒} {vol}^{*} (y ∖ B))$
71	63 67 70	3bitr4d	$⊢ φ \to (B^{\{A\}} \in dom voln (\{A\}) \leftrightarrow B \in dom vol)$

Metamath Proof Explorer

Theorem vonvolmbl

Proof