volmeas

Description: The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017)

		Ref	Expression
	Assertion	volmeas	$⊢ vol \in measures (dom vol)$

Proof

Step	Hyp	Ref	Expression
1		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
2		fvssunirn	$⊢ sigAlgebra (ℝ) \subseteq ⋃ ran sigAlgebra$
3		dmvlsiga	$⊢ dom vol \in sigAlgebra (ℝ)$
4	2 3	sselii	$⊢ dom vol \in ⋃ ran sigAlgebra$
5		0elsiga	$⊢ dom vol \in ⋃ ran sigAlgebra \to \emptyset \in dom vol$
6	4 5	ax-mp	$⊢ \emptyset \in dom vol$
7		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
8	6 7	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
9		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
10	8 9	eqtri	$⊢ vol (\emptyset) = 0$
11		simpr	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \to x \in Fin$
12		nfv	$⊢ Ⅎ y x \in 𝒫 dom vol$
13		nfv	$⊢ Ⅎ y x ≼ ω$
14		nfdisj1	$⊢ Ⅎ y \underset{y \in x}{Disj} y$
15	13 14	nfan	$⊢ Ⅎ y (x ≼ ω \land \underset{y \in x}{Disj} y)$
16	12 15	nfan	$⊢ Ⅎ y (x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y))$
17		nfv	$⊢ Ⅎ y x \in Fin$
18	16 17	nfan	$⊢ Ⅎ y ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin)$
19		elpwi	$⊢ x \in 𝒫 dom vol \to x \subseteq dom vol$
20	19	ad3antrrr	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \land y \in x) \to x \subseteq dom vol$
21		simpr	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \land y \in x) \to y \in x$
22	20 21	sseldd	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \land y \in x) \to y \in dom vol$
23	22	ex	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \to (y \in x \to y \in dom vol)$
24	18 23	ralrimi	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \to \forall y \in x y \in dom vol$
25		simplrr	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \to \underset{y \in x}{Disj} y$
26		uniiun	$⊢ ⋃ x = ⋃_{y \in x} y$
27	26	fveq2i	$⊢ vol (⋃ x) = vol (⋃_{y \in x} y)$
28		volfiniune	$⊢ (x \in Fin \land \forall y \in x y \in dom vol \land \underset{y \in x}{Disj} y) \to vol (⋃_{y \in x} y) = \underset{y \in x}{\sum^{*}} vol (y)$
29	27 28	syl5eq	$⊢ (x \in Fin \land \forall y \in x y \in dom vol \land \underset{y \in x}{Disj} y) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
30	11 24 25 29	syl3anc	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x \in Fin) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
31		bren	$⊢ ℕ \approx x \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} x$
32		nfv	$⊢ Ⅎ n (x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x)$
33		nfcv	$⊢ \underline{Ⅎ} n vol (y)$
34		nfcv	$⊢ \underline{Ⅎ} y vol (f (n))$
35		nfcv	$⊢ \underline{Ⅎ} n x$
36		nfcv	$⊢ \underline{Ⅎ} n ℕ$
37		nfcv	$⊢ \underline{Ⅎ} n f$
38		fveq2	$⊢ y = f (n) \to vol (y) = vol (f (n))$
39		simpl	$⊢ (x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \to x \in 𝒫 dom vol$
40		simpr	$⊢ (x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \to f : ℕ \underset{1-1 onto}{⟶} x$
41		eqidd	$⊢ ((x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \land n \in ℕ) \to f (n) = f (n)$
42	1	a1i	$⊢ ((x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \land y \in x) \to vol : dom vol ⟶ [0, +∞]$
43	39 19	syl	$⊢ (x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \to x \subseteq dom vol$
44	43	sselda	$⊢ ((x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \land y \in x) \to y \in dom vol$
45	42 44	ffvelrnd	$⊢ ((x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \land y \in x) \to vol (y) \in [0, +∞]$
46	32 33 34 35 36 37 38 39 40 41 45	esumf1o	$⊢ (x \in 𝒫 dom vol \land f : ℕ \underset{1-1 onto}{⟶} x) \to \underset{y \in x}{\sum^{}} vol (y) = \underset{n \in ℕ}{\sum^{}} vol (f (n))$
47	46	adantlr	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to \underset{y \in x}{\sum^{}} vol (y) = \underset{n \in ℕ}{\sum^{}} vol (f (n))$
48	19	ad3antrrr	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \land n \in ℕ) \to x \subseteq dom vol$
49		f1of	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to f : ℕ ⟶ x$
50	49	adantl	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to f : ℕ ⟶ x$
51	50	ffvelrnda	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \land n \in ℕ) \to f (n) \in x$
52	48 51	sseldd	$⊢ (((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \land n \in ℕ) \to f (n) \in dom vol$
53	52	ralrimiva	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to \forall n \in ℕ f (n) \in dom vol$
54		simpr	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to f : ℕ \underset{1-1 onto}{⟶} x$
55		simplrr	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to \underset{y \in x}{Disj} y$
56		id	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to f : ℕ \underset{1-1 onto}{⟶} x$
57		simpr	$⊢ (f : ℕ \underset{1-1 onto}{⟶} x \land y = f (n)) \to y = f (n)$
58	56 57	disjrdx	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to (\underset{n \in ℕ}{Disj} f (n) \leftrightarrow \underset{y \in x}{Disj} y)$
59	58	biimpar	$⊢ (f : ℕ \underset{1-1 onto}{⟶} x \land \underset{y \in x}{Disj} y) \to \underset{n \in ℕ}{Disj} f (n)$
60	54 55 59	syl2anc	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to \underset{n \in ℕ}{Disj} f (n)$
61		voliune	$⊢ (\forall n \in ℕ f (n) \in dom vol \land \underset{n \in ℕ}{Disj} f (n)) \to vol (⋃_{n \in ℕ} f (n)) = \underset{n \in ℕ}{\sum^{*}} vol (f (n))$
62	53 60 61	syl2anc	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to vol (⋃_{n \in ℕ} f (n)) = \underset{n \in ℕ}{\sum^{*}} vol (f (n))$
63		f1ofo	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to f : ℕ \underset{onto}{⟶} x$
64	63 57	iunrdx	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃_{y \in x} y$
65	64 26	eqtr4di	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃ x$
66	65	fveq2d	$⊢ f : ℕ \underset{1-1 onto}{⟶} x \to vol (⋃_{n \in ℕ} f (n)) = vol (⋃ x)$
67	66	adantl	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to vol (⋃_{n \in ℕ} f (n)) = vol (⋃ x)$
68	47 62 67	3eqtr2rd	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land f : ℕ \underset{1-1 onto}{⟶} x) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
69	68	ex	$⊢ (x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to (f : ℕ \underset{1-1 onto}{⟶} x \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y))$
70	69	exlimdv	$⊢ (x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to (\exists f f : ℕ \underset{1-1 onto}{⟶} x \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y))$
71	70	imp	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \exists f f : ℕ \underset{1-1 onto}{⟶} x) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
72	31 71	sylan2b	$⊢ ((x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land ℕ \approx x) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
73		brdom2	$⊢ x ≼ ω \leftrightarrow (x ≺ ω \lor x \approx ω)$
74	73	biimpi	$⊢ x ≼ ω \to (x ≺ ω \lor x \approx ω)$
75		isfinite2	$⊢ x ≺ ω \to x \in Fin$
76		ensymb	$⊢ x \approx ω \leftrightarrow ω \approx x$
77		nnenom	$⊢ ℕ \approx ω$
78		entr	$⊢ (ℕ \approx ω \land ω \approx x) \to ℕ \approx x$
79	77 78	mpan	$⊢ ω \approx x \to ℕ \approx x$
80	76 79	sylbi	$⊢ x \approx ω \to ℕ \approx x$
81	75 80	orim12i	$⊢ (x ≺ ω \lor x \approx ω) \to (x \in Fin \lor ℕ \approx x)$
82	74 81	syl	$⊢ x ≼ ω \to (x \in Fin \lor ℕ \approx x)$
83	82	ad2antrl	$⊢ (x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to (x \in Fin \lor ℕ \approx x)$
84	30 72 83	mpjaodan	$⊢ (x \in 𝒫 dom vol \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)$
85	84	ex	$⊢ x \in 𝒫 dom vol \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y))$
86	85	rgen	$⊢ \forall x \in 𝒫 dom vol ((x ≼ ω \land \underset{y \in x}{Disj} y) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y))$
87		ismeas	$⊢ dom vol \in ⋃ ran sigAlgebra \to (vol \in measures (dom vol) \leftrightarrow (vol : dom vol ⟶ [0, +∞] \land vol (\emptyset) = 0 \land \forall x \in 𝒫 dom vol ((x ≼ ω \land \underset{y \in x}{Disj} y) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y))))$
88	4 87	ax-mp	$⊢ vol \in measures (dom vol) \leftrightarrow (vol : dom vol ⟶ [0, +∞] \land vol (\emptyset) = 0 \land \forall x \in 𝒫 dom vol ((x ≼ ω \land \underset{y \in x}{Disj} y) \to vol (⋃ x) = \underset{y \in x}{\sum^{*}} vol (y)))$
89	1 10 86 88	mpbir3an	$⊢ vol \in measures (dom vol)$

Metamath Proof Explorer

Theorem volmeas

Proof