meascnbl

Description: A measure is continuous from below. Cf. volsup . (Contributed by Thierry Arnoux, 18-Jan-2017) (Revised by Thierry Arnoux, 11-Jul-2017)

	Ref	Expression
Hypotheses	meascnbl.0	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
	meascnbl.1	$⊢ φ \to M \in measures (S)$
	meascnbl.2	$⊢ φ \to F : ℕ ⟶ S$
	meascnbl.3	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)$
Assertion	meascnbl	$⊢ φ \to (M \circ F) \underset{t}{⇝} (J) M (⋃ ran F)$

Proof

Step	Hyp	Ref	Expression
1		meascnbl.0	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
2		meascnbl.1	$⊢ φ \to M \in measures (S)$
3		meascnbl.2	$⊢ φ \to F : ℕ ⟶ S$
4		meascnbl.3	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)$
5	2	adantr	$⊢ (φ \land n \in ℕ) \to M \in measures (S)$
6		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
7	2 6	syl	$⊢ φ \to S \in ⋃ ran sigAlgebra$
8	7	adantr	$⊢ (φ \land n \in ℕ) \to S \in ⋃ ran sigAlgebra$
9	3	ffvelrnda	$⊢ (φ \land n \in ℕ) \to F (n) \in S$
10		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 ..^n)) \to φ$
11		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
12		simpr	$⊢ ((φ \land n \in ℕ) \land k \in (1 ..^n)) \to k \in (1 ..^n)$
13	11 12	sselid	$⊢ ((φ \land n \in ℕ) \land k \in (1 ..^n)) \to k \in ℕ$
14	3	ffvelrnda	$⊢ (φ \land k \in ℕ) \to F (k) \in S$
15	10 13 14	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 ..^n)) \to F (k) \in S$
16	15	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall k \in (1 ..^n) F (k) \in S$
17		sigaclfu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^n) F (k) \in S) \to ⋃_{k \in (1 ..^n)} F (k) \in S$
18	8 16 17	syl2anc	$⊢ (φ \land n \in ℕ) \to ⋃_{k \in (1 ..^n)} F (k) \in S$
19		difelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land F (n) \in S \land ⋃_{k \in (1 ..^n)} F (k) \in S) \to F (n) ∖ ⋃_{k \in (1 ..^n)} F (k) \in S$
20	8 9 18 19	syl3anc	$⊢ (φ \land n \in ℕ) \to F (n) ∖ ⋃_{k \in (1 ..^n)} F (k) \in S$
21		measvxrge0	$⊢ (M \in measures (S) \land F (n) ∖ ⋃_{k \in (1 ..^n)} F (k) \in S) \to M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)) \in [0, +∞]$
22	5 20 21	syl2anc	$⊢ (φ \land n \in ℕ) \to M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)) \in [0, +∞]$
23		fveq2	$⊢ n = o \to F (n) = F (o)$
24		oveq2	$⊢ n = o \to (1 ..^n) = (1 ..^o)$
25	24	iuneq1d	$⊢ n = o \to ⋃_{k \in (1 ..^n)} F (k) = ⋃_{k \in (1 ..^o)} F (k)$
26	23 25	difeq12d	$⊢ n = o \to F (n) ∖ ⋃_{k \in (1 ..^n)} F (k) = F (o) ∖ ⋃_{k \in (1 ..^o)} F (k)$
27	26	fveq2d	$⊢ n = o \to M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)) = M (F (o) ∖ ⋃_{k \in (1 ..^o)} F (k))$
28		fveq2	$⊢ n = p \to F (n) = F (p)$
29		oveq2	$⊢ n = p \to (1 ..^n) = (1 ..^p)$
30	29	iuneq1d	$⊢ n = p \to ⋃_{k \in (1 ..^n)} F (k) = ⋃_{k \in (1 ..^p)} F (k)$
31	28 30	difeq12d	$⊢ n = p \to F (n) ∖ ⋃_{k \in (1 ..^n)} F (k) = F (p) ∖ ⋃_{k \in (1 ..^p)} F (k)$
32	31	fveq2d	$⊢ n = p \to M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)) = M (F (p) ∖ ⋃_{k \in (1 ..^p)} F (k))$
33	1 22 27 32	esumcvg2	$⊢ φ \to (i \in ℕ ⟼ {\sum^{}}_{n = 1}^{i} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))) \underset{t}{⇝} (J) \underset{n \in ℕ}{\sum^{}} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))$
34		measfrge0	$⊢ M \in measures (S) \to M : S ⟶ [0, +∞]$
35	2 34	syl	$⊢ φ \to M : S ⟶ [0, +∞]$
36		fcompt	$⊢ (M : S ⟶ [0, +∞] \land F : ℕ ⟶ S) \to M \circ F = (i \in ℕ ⟼ M (F (i)))$
37	35 3 36	syl2anc	$⊢ φ \to M \circ F = (i \in ℕ ⟼ M (F (i)))$
38		nfcv	$⊢ \underline{Ⅎ} n F (k)$
39		fveq2	$⊢ n = k \to F (n) = F (k)$
40		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
41	40	nnzd	$⊢ (φ \land i \in ℕ) \to i \in ℤ$
42		fzval3	$⊢ i \in ℤ \to (1 \dots i) = (1 ..^i + 1)$
43	41 42	syl	$⊢ (φ \land i \in ℕ) \to (1 \dots i) = (1 ..^i + 1)$
44	43	olcd	$⊢ (φ \land i \in ℕ) \to ((1 \dots i) = ℕ \lor (1 \dots i) = (1 ..^i + 1))$
45	2	adantr	$⊢ (φ \land i \in ℕ) \to M \in measures (S)$
46		simpll	$⊢ ((φ \land i \in ℕ) \land n \in (1 \dots i)) \to φ$
47		fzossnn	$⊢ (1 ..^i + 1) \subseteq ℕ$
48	43	eleq2d	$⊢ (φ \land i \in ℕ) \to (n \in (1 \dots i) \leftrightarrow n \in (1 ..^i + 1))$
49	48	biimpa	$⊢ ((φ \land i \in ℕ) \land n \in (1 \dots i)) \to n \in (1 ..^i + 1)$
50	47 49	sselid	$⊢ ((φ \land i \in ℕ) \land n \in (1 \dots i)) \to n \in ℕ$
51	46 50 9	syl2anc	$⊢ ((φ \land i \in ℕ) \land n \in (1 \dots i)) \to F (n) \in S$
52	38 39 44 45 51	measiuns	$⊢ (φ \land i \in ℕ) \to M (⋃_{n = 1}^{i} F (n)) = {\sum^{*}}_{n = 1}^{i} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))$
53	3	ffnd	$⊢ φ \to F Fn ℕ$
54	53 4	iuninc	$⊢ (φ \land i \in ℕ) \to ⋃_{n = 1}^{i} F (n) = F (i)$
55	54	fveq2d	$⊢ (φ \land i \in ℕ) \to M (⋃_{n = 1}^{i} F (n)) = M (F (i))$
56	52 55	eqtr3d	$⊢ (φ \land i \in ℕ) \to {\sum^{*}}_{n = 1}^{i} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)) = M (F (i))$
57	56	mpteq2dva	$⊢ φ \to (i \in ℕ ⟼ {\sum^{*}}_{n = 1}^{i} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))) = (i \in ℕ ⟼ M (F (i)))$
58	37 57	eqtr4d	$⊢ φ \to M \circ F = (i \in ℕ ⟼ {\sum^{*}}_{n = 1}^{i} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k)))$
59	9	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) \in S$
60		dfiun2g	$⊢ \forall n \in ℕ F (n) \in S \to ⋃_{n \in ℕ} F (n) = ⋃ \{x \| \exists n \in ℕ x = F (n)\}$
61	59 60	syl	$⊢ φ \to ⋃_{n \in ℕ} F (n) = ⋃ \{x \| \exists n \in ℕ x = F (n)\}$
62		fnrnfv	$⊢ F Fn ℕ \to ran F = \{x \| \exists n \in ℕ x = F (n)\}$
63	53 62	syl	$⊢ φ \to ran F = \{x \| \exists n \in ℕ x = F (n)\}$
64	63	unieqd	$⊢ φ \to ⋃ ran F = ⋃ \{x \| \exists n \in ℕ x = F (n)\}$
65	61 64	eqtr4d	$⊢ φ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
66	65	fveq2d	$⊢ φ \to M (⋃_{n \in ℕ} F (n)) = M (⋃ ran F)$
67		eqidd	$⊢ φ \to ℕ = ℕ$
68	67	orcd	$⊢ φ \to (ℕ = ℕ \lor ℕ = (1 ..^i + 1))$
69	38 39 68 2 9	measiuns	$⊢ φ \to M (⋃_{n \in ℕ} F (n)) = \underset{n \in ℕ}{\sum^{*}} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))$
70	66 69	eqtr3d	$⊢ φ \to M (⋃ ran F) = \underset{n \in ℕ}{\sum^{*}} M (F (n) ∖ ⋃_{k \in (1 ..^n)} F (k))$
71	33 58 70	3brtr4d	$⊢ φ \to (M \circ F) \underset{t}{⇝} (J) M (⋃ ran F)$

Metamath Proof Explorer

Theorem meascnbl

Proof