measiuns

Description: The measure of the union of a collection of sets, expressed as the sum of a disjoint set. This is used as a lemma for both measiun and meascnbl . (Contributed by Thierry Arnoux, 22-Jan-2017) (Proof shortened by Thierry Arnoux, 7-Feb-2017)

	Ref	Expression
Hypotheses	measiuns.0	$⊢ \underline{Ⅎ} n B$
	measiuns.1	$⊢ n = k \to A = B$
	measiuns.2	$⊢ φ \to (N = ℕ \lor N = (1 ..^I))$
	measiuns.3	$⊢ φ \to M \in measures (S)$
	measiuns.4	$⊢ (φ \land n \in N) \to A \in S$
Assertion	measiuns	$⊢ φ \to M (⋃_{n \in N} A) = \underset{n \in N}{\sum^{*}} M (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

Step	Hyp	Ref	Expression
1		measiuns.0	$⊢ \underline{Ⅎ} n B$
2		measiuns.1	$⊢ n = k \to A = B$
3		measiuns.2	$⊢ φ \to (N = ℕ \lor N = (1 ..^I))$
4		measiuns.3	$⊢ φ \to M \in measures (S)$
5		measiuns.4	$⊢ (φ \land n \in N) \to A \in S$
6	1 2 3	iundisjcnt	$⊢ φ \to ⋃_{n \in N} A = ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)$
7	6	fveq2d	$⊢ φ \to M (⋃_{n \in N} A) = M (⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B))$
8		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
9	4 8	syl	$⊢ φ \to S \in ⋃ ran sigAlgebra$
10	9	adantr	$⊢ (φ \land n \in N) \to S \in ⋃ ran sigAlgebra$
11		simpll	$⊢ ((φ \land n \in N) \land k \in (1 ..^n)) \to φ$
12		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
13		simpr	$⊢ ((φ \land n \in N) \land N = ℕ) \to N = ℕ$
14	12 13	sseqtrrid	$⊢ ((φ \land n \in N) \land N = ℕ) \to (1 ..^n) \subseteq N$
15		simplr	$⊢ ((φ \land n \in N) \land N = (1 ..^I)) \to n \in N$
16		simpr	$⊢ ((φ \land n \in N) \land N = (1 ..^I)) \to N = (1 ..^I)$
17	15 16	eleqtrd	$⊢ ((φ \land n \in N) \land N = (1 ..^I)) \to n \in (1 ..^I)$
18		elfzouz2	$⊢ n \in (1 ..^I) \to I \in ℤ_{\geq n}$
19		fzoss2	$⊢ I \in ℤ_{\geq n} \to (1 ..^n) \subseteq (1 ..^I)$
20	17 18 19	3syl	$⊢ ((φ \land n \in N) \land N = (1 ..^I)) \to (1 ..^n) \subseteq (1 ..^I)$
21	20 16	sseqtrrd	$⊢ ((φ \land n \in N) \land N = (1 ..^I)) \to (1 ..^n) \subseteq N$
22	3	adantr	$⊢ (φ \land n \in N) \to (N = ℕ \lor N = (1 ..^I))$
23	14 21 22	mpjaodan	$⊢ (φ \land n \in N) \to (1 ..^n) \subseteq N$
24	23	sselda	$⊢ ((φ \land n \in N) \land k \in (1 ..^n)) \to k \in N$
25	5	sbimi	$⊢ [k/ n] (φ \land n \in N) \to [k/ n] A \in S$
26		sban	$⊢ [k/ n] (φ \land n \in N) \leftrightarrow ([k/ n] φ \land [k/ n] n \in N)$
27		sbv	$⊢ [k/ n] φ \leftrightarrow φ$
28		clelsb1	$⊢ [k/ n] n \in N \leftrightarrow k \in N$
29	27 28	anbi12i	$⊢ ([k/ n] φ \land [k/ n] n \in N) \leftrightarrow (φ \land k \in N)$
30	26 29	bitri	$⊢ [k/ n] (φ \land n \in N) \leftrightarrow (φ \land k \in N)$
31		sbsbc	$⊢ [k/ n] A \in S \leftrightarrow \underset{˙}{[} k / n \underset{˙}{]} A \in S$
32		sbcel1g	$⊢ k \in V \to (\underset{˙}{[} k / n \underset{˙}{]} A \in S \leftrightarrow ⦋ k / n ⦌ A \in S)$
33	32	elv	$⊢ \underset{˙}{[} k / n \underset{˙}{]} A \in S \leftrightarrow ⦋ k / n ⦌ A \in S$
34		nfcv	$⊢ \underline{Ⅎ} k A$
35	34 1 2	cbvcsbw	$⊢ ⦋ k / n ⦌ A = ⦋ k / k ⦌ B$
36		csbid	$⊢ ⦋ k / k ⦌ B = B$
37	35 36	eqtri	$⊢ ⦋ k / n ⦌ A = B$
38	37	eleq1i	$⊢ ⦋ k / n ⦌ A \in S \leftrightarrow B \in S$
39	31 33 38	3bitri	$⊢ [k/ n] A \in S \leftrightarrow B \in S$
40	25 30 39	3imtr3i	$⊢ (φ \land k \in N) \to B \in S$
41	11 24 40	syl2anc	$⊢ ((φ \land n \in N) \land k \in (1 ..^n)) \to B \in S$
42	41	ralrimiva	$⊢ (φ \land n \in N) \to \forall k \in (1 ..^n) B \in S$
43		sigaclfu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^n) B \in S) \to ⋃_{k \in (1 ..^n)} B \in S$
44	10 42 43	syl2anc	$⊢ (φ \land n \in N) \to ⋃_{k \in (1 ..^n)} B \in S$
45		difelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land ⋃_{k \in (1 ..^n)} B \in S) \to A ∖ ⋃_{k \in (1 ..^n)} B \in S$
46	10 5 44 45	syl3anc	$⊢ (φ \land n \in N) \to A ∖ ⋃_{k \in (1 ..^n)} B \in S$
47	46	ralrimiva	$⊢ φ \to \forall n \in N A ∖ ⋃_{k \in (1 ..^n)} B \in S$
48		eqimss	$⊢ N = ℕ \to N \subseteq ℕ$
49		fzossnn	$⊢ (1 ..^I) \subseteq ℕ$
50		sseq1	$⊢ N = (1 ..^I) \to (N \subseteq ℕ \leftrightarrow (1 ..^I) \subseteq ℕ)$
51	49 50	mpbiri	$⊢ N = (1 ..^I) \to N \subseteq ℕ$
52	48 51	jaoi	$⊢ (N = ℕ \lor N = (1 ..^I)) \to N \subseteq ℕ$
53	3 52	syl	$⊢ φ \to N \subseteq ℕ$
54		nnct	$⊢ ℕ ≼ ω$
55		ssct	$⊢ (N \subseteq ℕ \land ℕ ≼ ω) \to N ≼ ω$
56	53 54 55	sylancl	$⊢ φ \to N ≼ ω$
57	1 2 3	iundisj2cnt	$⊢ φ \to \underset{n \in N}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$
58		measvuni	$⊢ (M \in measures (S) \land \forall n \in N A ∖ ⋃_{k \in (1 ..^n)} B \in S \land (N ≼ ω \land \underset{n \in N}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B))) \to M (⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)) = \underset{n \in N}{\sum^{*}} M (A ∖ ⋃_{k \in (1 ..^n)} B)$
59	4 47 56 57 58	syl112anc	$⊢ φ \to M (⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)) = \underset{n \in N}{\sum^{*}} M (A ∖ ⋃_{k \in (1 ..^n)} B)$
60	7 59	eqtrd	$⊢ φ \to M (⋃_{n \in N} A) = \underset{n \in N}{\sum^{*}} M (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer

Theorem measiuns

Proof