volfiniune

Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun what voliune is to voliun . (Contributed by Thierry Arnoux, 16-Oct-2017)

		Ref	Expression
	Assertion	volfiniune	$⊢ (A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \to vol (⋃_{n \in A} B) = \underset{n \in A}{\sum^{*}} vol (B)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to A \in Fin$
2		simpl2	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to \forall n \in A B \in dom vol$
3		simpr	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to \forall n \in A vol (B) \in ℝ$
4		r19.26	$⊢ \forall n \in A (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow (\forall n \in A B \in dom vol \land \forall n \in A vol (B) \in ℝ)$
5	2 3 4	sylanbrc	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to \forall n \in A (B \in dom vol \land vol (B) \in ℝ)$
6		simpl3	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to \underset{n \in A}{Disj} B$
7		volfiniun	$⊢ (A \in Fin \land \forall n \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{n \in A}{Disj} B) \to vol (⋃_{n \in A} B) = \sum_{n \in A} vol (B)$
8	1 5 6 7	syl3anc	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to vol (⋃_{n \in A} B) = \sum_{n \in A} vol (B)$
9		nfcv	$⊢ \underline{Ⅎ} n A$
10	9	nfel1	$⊢ Ⅎ n A \in Fin$
11		nfra1	$⊢ Ⅎ n \forall n \in A B \in dom vol$
12		nfdisj1	$⊢ Ⅎ n \underset{n \in A}{Disj} B$
13	10 11 12	nf3an	$⊢ Ⅎ n (A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B)$
14		nfra1	$⊢ Ⅎ n \forall n \in A vol (B) \in ℝ$
15	13 14	nfan	$⊢ Ⅎ n ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ)$
16	3	r19.21bi	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \land n \in A) \to vol (B) \in ℝ$
17		rspa	$⊢ (\forall n \in A B \in dom vol \land n \in A) \to B \in dom vol$
18		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
19	18	ffvelrni	$⊢ B \in dom vol \to vol (B) \in [0, +∞]$
20	17 19	syl	$⊢ (\forall n \in A B \in dom vol \land n \in A) \to vol (B) \in [0, +∞]$
21	2 20	sylan	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \land n \in A) \to vol (B) \in [0, +∞]$
22		0xr	$⊢ 0 \in ℝ^{*}$
23		pnfxr	$⊢ +∞ \in ℝ^{*}$
24		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (vol (B) \in [0, +∞] \leftrightarrow (vol (B) \in ℝ^{*} \land 0 \leq vol (B) \land vol (B) \leq +∞))$
25	22 23 24	mp2an	$⊢ vol (B) \in [0, +∞] \leftrightarrow (vol (B) \in ℝ^{*} \land 0 \leq vol (B) \land vol (B) \leq +∞)$
26	25	simp2bi	$⊢ vol (B) \in [0, +∞] \to 0 \leq vol (B)$
27	21 26	syl	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \land n \in A) \to 0 \leq vol (B)$
28		ltpnf	$⊢ vol (B) \in ℝ \to vol (B) < +∞$
29	16 28	syl	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \land n \in A) \to vol (B) < +∞$
30		0re	$⊢ 0 \in ℝ$
31		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (vol (B) \in [0, +∞) \leftrightarrow (vol (B) \in ℝ \land 0 \leq vol (B) \land vol (B) < +∞))$
32	30 23 31	mp2an	$⊢ vol (B) \in [0, +∞) \leftrightarrow (vol (B) \in ℝ \land 0 \leq vol (B) \land vol (B) < +∞)$
33	16 27 29 32	syl3anbrc	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \land n \in A) \to vol (B) \in [0, +∞)$
34	9 15 1 33	esumpfinvalf	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to \underset{n \in A}{\sum^{*}} vol (B) = \sum_{n \in A} vol (B)$
35	8 34	eqtr4d	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \forall n \in A vol (B) \in ℝ) \to vol (⋃_{n \in A} B) = \underset{n \in A}{\sum^{*}} vol (B)$
36		simpr	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \exists n \in A vol (B) = +∞$
37		nfv	$⊢ Ⅎ k vol (B) = +∞$
38		nfcv	$⊢ \underline{Ⅎ} n vol$
39		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ k / n ⦌ B$
40	38 39	nffv	$⊢ \underline{Ⅎ} n vol (⦋ k / n ⦌ B)$
41	40	nfeq1	$⊢ Ⅎ n vol (⦋ k / n ⦌ B) = +∞$
42		csbeq1a	$⊢ n = k \to B = ⦋ k / n ⦌ B$
43	42	fveqeq2d	$⊢ n = k \to (vol (B) = +∞ \leftrightarrow vol (⦋ k / n ⦌ B) = +∞)$
44	37 41 43	cbvrexw	$⊢ \exists n \in A vol (B) = +∞ \leftrightarrow \exists k \in A vol (⦋ k / n ⦌ B) = +∞$
45	36 44	sylib	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \exists k \in A vol (⦋ k / n ⦌ B) = +∞$
46	39	nfel1	$⊢ Ⅎ n ⦋ k / n ⦌ B \in dom vol$
47	42	eleq1d	$⊢ n = k \to (B \in dom vol \leftrightarrow ⦋ k / n ⦌ B \in dom vol)$
48	46 47	rspc	$⊢ k \in A \to (\forall n \in A B \in dom vol \to ⦋ k / n ⦌ B \in dom vol)$
49	48	impcom	$⊢ (\forall n \in A B \in dom vol \land k \in A) \to ⦋ k / n ⦌ B \in dom vol$
50	49	adantll	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol) \land k \in A) \to ⦋ k / n ⦌ B \in dom vol$
51		finiunmbl	$⊢ (A \in Fin \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B \in dom vol$
52	51	adantr	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol) \land k \in A) \to ⋃_{n \in A} B \in dom vol$
53		nfcv	$⊢ \underline{Ⅎ} n k$
54	9 53 39 42	ssiun2sf	$⊢ k \in A \to ⦋ k / n ⦌ B \subseteq ⋃_{n \in A} B$
55	54	adantl	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol) \land k \in A) \to ⦋ k / n ⦌ B \subseteq ⋃_{n \in A} B$
56		volss	$⊢ (⦋ k / n ⦌ B \in dom vol \land ⋃_{n \in A} B \in dom vol \land ⦋ k / n ⦌ B \subseteq ⋃_{n \in A} B) \to vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)$
57	50 52 55 56	syl3anc	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol) \land k \in A) \to vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)$
58	57	3adantl3	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land k \in A) \to vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)$
59	58	adantlr	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \land k \in A) \to vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)$
60	59	ralrimiva	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \forall k \in A vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)$
61		r19.29r	$⊢ (\exists k \in A vol (⦋ k / n ⦌ B) = +∞ \land \forall k \in A vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)) \to \exists k \in A (vol (⦋ k / n ⦌ B) = +∞ \land vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B))$
62	45 60 61	syl2anc	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \exists k \in A (vol (⦋ k / n ⦌ B) = +∞ \land vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B))$
63		breq1	$⊢ vol (⦋ k / n ⦌ B) = +∞ \to (vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B) \leftrightarrow +∞ \leq vol (⋃_{n \in A} B))$
64	63	biimpa	$⊢ (vol (⦋ k / n ⦌ B) = +∞ \land vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)) \to +∞ \leq vol (⋃_{n \in A} B)$
65	64	reximi	$⊢ \exists k \in A (vol (⦋ k / n ⦌ B) = +∞ \land vol (⦋ k / n ⦌ B) \leq vol (⋃_{n \in A} B)) \to \exists k \in A +∞ \leq vol (⋃_{n \in A} B)$
66	62 65	syl	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \exists k \in A +∞ \leq vol (⋃_{n \in A} B)$
67		rexex	$⊢ \exists k \in A +∞ \leq vol (⋃_{n \in A} B) \to \exists k +∞ \leq vol (⋃_{n \in A} B)$
68		19.9v	$⊢ \exists k +∞ \leq vol (⋃_{n \in A} B) \leftrightarrow +∞ \leq vol (⋃_{n \in A} B)$
69	67 68	sylib	$⊢ \exists k \in A +∞ \leq vol (⋃_{n \in A} B) \to +∞ \leq vol (⋃_{n \in A} B)$
70	66 69	syl	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to +∞ \leq vol (⋃_{n \in A} B)$
71		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
72	18	ffvelrni	$⊢ ⋃_{n \in A} B \in dom vol \to vol (⋃_{n \in A} B) \in [0, +∞]$
73	71 72	sseldi	$⊢ ⋃_{n \in A} B \in dom vol \to vol (⋃_{n \in A} B) \in ℝ^{*}$
74	51 73	syl	$⊢ (A \in Fin \land \forall n \in A B \in dom vol) \to vol (⋃_{n \in A} B) \in ℝ^{*}$
75	74	3adant3	$⊢ (A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \to vol (⋃_{n \in A} B) \in ℝ^{*}$
76	75	adantr	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to vol (⋃_{n \in A} B) \in ℝ^{*}$
77		xgepnf	$⊢ vol (⋃_{n \in A} B) \in ℝ^{*} \to (+∞ \leq vol (⋃_{n \in A} B) \leftrightarrow vol (⋃_{n \in A} B) = +∞)$
78	76 77	syl	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to (+∞ \leq vol (⋃_{n \in A} B) \leftrightarrow vol (⋃_{n \in A} B) = +∞)$
79	70 78	mpbid	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to vol (⋃_{n \in A} B) = +∞$
80		nfre1	$⊢ Ⅎ n \exists n \in A vol (B) = +∞$
81	13 80	nfan	$⊢ Ⅎ n ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞)$
82		simpl1	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to A \in Fin$
83	20	3ad2antl2	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land n \in A) \to vol (B) \in [0, +∞]$
84	83	adantlr	$⊢ (((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \land n \in A) \to vol (B) \in [0, +∞]$
85	81 82 84 36	esumpinfval	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to \underset{n \in A}{\sum^{*}} vol (B) = +∞$
86	79 85	eqtr4d	$⊢ ((A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \land \exists n \in A vol (B) = +∞) \to vol (⋃_{n \in A} B) = \underset{n \in A}{\sum^{*}} vol (B)$
87		exmid	$⊢ (\forall n \in A vol (B) \in ℝ \lor \neg \forall n \in A vol (B) \in ℝ)$
88		rexnal	$⊢ \exists n \in A \neg vol (B) \in ℝ \leftrightarrow \neg \forall n \in A vol (B) \in ℝ$
89	88	orbi2i	$⊢ (\forall n \in A vol (B) \in ℝ \lor \exists n \in A \neg vol (B) \in ℝ) \leftrightarrow (\forall n \in A vol (B) \in ℝ \lor \neg \forall n \in A vol (B) \in ℝ)$
90	87 89	mpbir	$⊢ (\forall n \in A vol (B) \in ℝ \lor \exists n \in A \neg vol (B) \in ℝ)$
91		r19.29	$⊢ (\forall n \in A B \in dom vol \land \exists n \in A \neg vol (B) \in ℝ) \to \exists n \in A (B \in dom vol \land \neg vol (B) \in ℝ)$
92		xrge0nre	$⊢ (vol (B) \in [0, +∞] \land \neg vol (B) \in ℝ) \to vol (B) = +∞$
93	19 92	sylan	$⊢ (B \in dom vol \land \neg vol (B) \in ℝ) \to vol (B) = +∞$
94	93	reximi	$⊢ \exists n \in A (B \in dom vol \land \neg vol (B) \in ℝ) \to \exists n \in A vol (B) = +∞$
95	91 94	syl	$⊢ (\forall n \in A B \in dom vol \land \exists n \in A \neg vol (B) \in ℝ) \to \exists n \in A vol (B) = +∞$
96	95	ex	$⊢ \forall n \in A B \in dom vol \to (\exists n \in A \neg vol (B) \in ℝ \to \exists n \in A vol (B) = +∞)$
97	96	orim2d	$⊢ \forall n \in A B \in dom vol \to ((\forall n \in A vol (B) \in ℝ \lor \exists n \in A \neg vol (B) \in ℝ) \to (\forall n \in A vol (B) \in ℝ \lor \exists n \in A vol (B) = +∞))$
98	90 97	mpi	$⊢ \forall n \in A B \in dom vol \to (\forall n \in A vol (B) \in ℝ \lor \exists n \in A vol (B) = +∞)$
99	98	3ad2ant2	$⊢ (A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \to (\forall n \in A vol (B) \in ℝ \lor \exists n \in A vol (B) = +∞)$
100	35 86 99	mpjaodan	$⊢ (A \in Fin \land \forall n \in A B \in dom vol \land \underset{n \in A}{Disj} B) \to vol (⋃_{n \in A} B) = \underset{n \in A}{\sum^{*}} vol (B)$

Metamath Proof Explorer

Theorem volfiniune

Proof