measiun

Description: A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016) (Proof shortened by Thierry Arnoux, 7-Feb-2017)

	Ref	Expression
Hypotheses	measiun.1	$⊢ φ \to M \in measures (S)$
	measiun.2	$⊢ φ \to A \in S$
	measiun.3	$⊢ (φ \land n \in ℕ) \to B \in S$
	measiun.4	$⊢ φ \to A \subseteq ⋃_{n \in ℕ} B$
Assertion	measiun	$⊢ φ \to M (A) \leq \underset{n \in ℕ}{\sum^{*}} M (B)$

Proof

Step	Hyp	Ref	Expression
1		measiun.1	$⊢ φ \to M \in measures (S)$
2		measiun.2	$⊢ φ \to A \in S$
3		measiun.3	$⊢ (φ \land n \in ℕ) \to B \in S$
4		measiun.4	$⊢ φ \to A \subseteq ⋃_{n \in ℕ} B$
5		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
6		measvxrge0	$⊢ (M \in measures (S) \land A \in S) \to M (A) \in [0, +∞]$
7	1 2 6	syl2anc	$⊢ φ \to M (A) \in [0, +∞]$
8	5 7	sselid	$⊢ φ \to M (A) \in ℝ^{*}$
9		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
10	1 9	syl	$⊢ φ \to S \in ⋃ ran sigAlgebra$
11	3	ralrimiva	$⊢ φ \to \forall n \in ℕ B \in S$
12		sigaclcu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall n \in ℕ B \in S) \to ⋃_{n \in ℕ} B \in S$
13	10 11 12	syl2anc	$⊢ φ \to ⋃_{n \in ℕ} B \in S$
14		measvxrge0	$⊢ (M \in measures (S) \land ⋃_{n \in ℕ} B \in S) \to M (⋃_{n \in ℕ} B) \in [0, +∞]$
15	1 13 14	syl2anc	$⊢ φ \to M (⋃_{n \in ℕ} B) \in [0, +∞]$
16	5 15	sselid	$⊢ φ \to M (⋃_{n \in ℕ} B) \in ℝ^{*}$
17		nnex	$⊢ ℕ \in V$
18	1	adantr	$⊢ (φ \land n \in ℕ) \to M \in measures (S)$
19		measvxrge0	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in [0, +∞]$
20	18 3 19	syl2anc	$⊢ (φ \land n \in ℕ) \to M (B) \in [0, +∞]$
21	20	ralrimiva	$⊢ φ \to \forall n \in ℕ M (B) \in [0, +∞]$
22		nfcv	$⊢ \underline{Ⅎ} n ℕ$
23	22	esumcl	$⊢ (ℕ \in V \land \forall n \in ℕ M (B) \in [0, +∞]) \to \underset{n \in ℕ}{\sum^{*}} M (B) \in [0, +∞]$
24	17 21 23	sylancr	$⊢ φ \to \underset{n \in ℕ}{\sum^{*}} M (B) \in [0, +∞]$
25	5 24	sselid	$⊢ φ \to \underset{n \in ℕ}{\sum^{}} M (B) \in ℝ^{}$
26	1 2 13 4	measssd	$⊢ φ \to M (A) \leq M (⋃_{n \in ℕ} B)$
27		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ k / n ⦌ B$
28		csbeq1a	$⊢ n = k \to B = ⦋ k / n ⦌ B$
29		eqidd	$⊢ φ \to ℕ = ℕ$
30	29	orcd	$⊢ φ \to (ℕ = ℕ \lor ℕ = (1 ..^m))$
31	27 28 30 1 3	measiuns	$⊢ φ \to M (⋃_{n \in ℕ} B) = \underset{n \in ℕ}{\sum^{*}} M (B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B)$
32	17	a1i	$⊢ φ \to ℕ \in V$
33	10	adantr	$⊢ (φ \land n \in ℕ) \to S \in ⋃ ran sigAlgebra$
34		nfv	$⊢ Ⅎ n φ$
35		nfcv	$⊢ \underline{Ⅎ} n k$
36	35	nfel1	$⊢ Ⅎ n k \in ℕ$
37	27	nfel1	$⊢ Ⅎ n ⦋ k / n ⦌ B \in S$
38	36 37	nfim	$⊢ Ⅎ n (k \in ℕ \to ⦋ k / n ⦌ B \in S)$
39	34 38	nfim	$⊢ Ⅎ n (φ \to (k \in ℕ \to ⦋ k / n ⦌ B \in S))$
40		eleq1w	$⊢ n = k \to (n \in ℕ \leftrightarrow k \in ℕ)$
41	28	eleq1d	$⊢ n = k \to (B \in S \leftrightarrow ⦋ k / n ⦌ B \in S)$
42	40 41	imbi12d	$⊢ n = k \to ((n \in ℕ \to B \in S) \leftrightarrow (k \in ℕ \to ⦋ k / n ⦌ B \in S))$
43	42	imbi2d	$⊢ n = k \to ((φ \to (n \in ℕ \to B \in S)) \leftrightarrow (φ \to (k \in ℕ \to ⦋ k / n ⦌ B \in S)))$
44	3	ex	$⊢ φ \to (n \in ℕ \to B \in S)$
45	39 43 44	chvarfv	$⊢ φ \to (k \in ℕ \to ⦋ k / n ⦌ B \in S)$
46	45	ralrimiv	$⊢ φ \to \forall k \in ℕ ⦋ k / n ⦌ B \in S$
47		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
48		ssralv	$⊢ (1 ..^n) \subseteq ℕ \to (\forall k \in ℕ ⦋ k / n ⦌ B \in S \to \forall k \in (1 ..^n) ⦋ k / n ⦌ B \in S)$
49	47 48	ax-mp	$⊢ \forall k \in ℕ ⦋ k / n ⦌ B \in S \to \forall k \in (1 ..^n) ⦋ k / n ⦌ B \in S$
50		sigaclfu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^n) ⦋ k / n ⦌ B \in S) \to ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
51	49 50	sylan2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in ℕ ⦋ k / n ⦌ B \in S) \to ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
52	10 46 51	syl2anc	$⊢ φ \to ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
53	52	adantr	$⊢ (φ \land n \in ℕ) \to ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
54		difelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land B \in S \land ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S) \to B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
55	33 3 53 54	syl3anc	$⊢ (φ \land n \in ℕ) \to B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S$
56		measvxrge0	$⊢ (M \in measures (S) \land B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \in S) \to M (B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B) \in [0, +∞]$
57	18 55 56	syl2anc	$⊢ (φ \land n \in ℕ) \to M (B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B) \in [0, +∞]$
58		difssd	$⊢ (φ \land n \in ℕ) \to B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B \subseteq B$
59	18 55 3 58	measssd	$⊢ (φ \land n \in ℕ) \to M (B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B) \leq M (B)$
60	32 57 20 59	esumle	$⊢ φ \to \underset{n \in ℕ}{\sum^{}} M (B ∖ ⋃_{k \in (1 ..^n)} ⦋ k / n ⦌ B) \leq \underset{n \in ℕ}{\sum^{}} M (B)$
61	31 60	eqbrtrd	$⊢ φ \to M (⋃_{n \in ℕ} B) \leq \underset{n \in ℕ}{\sum^{*}} M (B)$
62	8 16 25 26 61	xrletrd	$⊢ φ \to M (A) \leq \underset{n \in ℕ}{\sum^{*}} M (B)$

Metamath Proof Explorer

Theorem measiun

Proof