meadjiun

Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meadjiun.1	$⊢ Ⅎ k φ$
	meadjiun.m	$⊢ φ \to M \in Meas$
	meadjiun.s	$⊢ S = dom M$
	meadjiun.b	$⊢ (φ \land k \in A) \to B \in S$
	meadjiun.a	$⊢ φ \to A ≼ ω$
	meadjiun.dj	$⊢ φ \to \underset{k \in A}{Disj} B$
Assertion	meadjiun	$⊢ φ \to M (⋃_{k \in A} B) = sum^((k \in A ⟼ M (B)))$

Proof

Step	Hyp	Ref	Expression
1		meadjiun.1	$⊢ Ⅎ k φ$
2		meadjiun.m	$⊢ φ \to M \in Meas$
3		meadjiun.s	$⊢ S = dom M$
4		meadjiun.b	$⊢ (φ \land k \in A) \to B \in S$
5		meadjiun.a	$⊢ φ \to A ≼ ω$
6		meadjiun.dj	$⊢ φ \to \underset{k \in A}{Disj} B$
7	4	ex	$⊢ φ \to (k \in A \to B \in S)$
8	1 7	ralrimi	$⊢ φ \to \forall k \in A B \in S$
9		dfiun3g	$⊢ \forall k \in A B \in S \to ⋃_{k \in A} B = ⋃ ran (k \in A ⟼ B)$
10	8 9	syl	$⊢ φ \to ⋃_{k \in A} B = ⋃ ran (k \in A ⟼ B)$
11	10	fveq2d	$⊢ φ \to M (⋃_{k \in A} B) = M (⋃ ran (k \in A ⟼ B))$
12		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
13	12	rnmptss	$⊢ \forall k \in A B \in S \to ran (k \in A ⟼ B) \subseteq S$
14	8 13	syl	$⊢ φ \to ran (k \in A ⟼ B) \subseteq S$
15		1stcrestlem	$⊢ A ≼ ω \to ran (k \in A ⟼ B) ≼ ω$
16	5 15	syl	$⊢ φ \to ran (k \in A ⟼ B) ≼ ω$
17	12	disjrnmpt2	$⊢ \underset{k \in A}{Disj} B \to \underset{x \in ran (k \in A ⟼ B)}{Disj} x$
18	6 17	syl	$⊢ φ \to \underset{x \in ran (k \in A ⟼ B)}{Disj} x$
19	2 3 14 16 18	meadjuni	$⊢ φ \to M (⋃ ran (k \in A ⟼ B)) = sum^({M ↾}_{ran (k \in A ⟼ B)})$
20		reldom	$⊢ Rel ≼$
21		brrelex1	$⊢ (Rel ≼ \land A ≼ ω) \to A \in V$
22	20 21	mpan	$⊢ A ≼ ω \to A \in V$
23	5 22	syl	$⊢ φ \to A \in V$
24	1 4 12	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ S$
25		fveq2	$⊢ j = i \to (k \in A ⟼ B) (j) = (k \in A ⟼ B) (i)$
26	25	neeq1d	$⊢ j = i \to ((k \in A ⟼ B) (j) \neq \emptyset \leftrightarrow (k \in A ⟼ B) (i) \neq \emptyset)$
27	26	cbvrabv	$⊢ \{j \in A \| (k \in A ⟼ B) (j) \neq \emptyset\} = \{i \in A \| (k \in A ⟼ B) (i) \neq \emptyset\}$
28		simpr	$⊢ (φ \land i \in A) \to i \in A$
29		nfv	$⊢ Ⅎ k i \in A$
30	1 29	nfan	$⊢ Ⅎ k (φ \land i \in A)$
31		nfcv	$⊢ \underline{Ⅎ} k i$
32	31	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ B$
33		nfcv	$⊢ \underline{Ⅎ} k S$
34	32 33	nfel	$⊢ Ⅎ k ⦋ i / k ⦌ B \in S$
35	30 34	nfim	$⊢ Ⅎ k ((φ \land i \in A) \to ⦋ i / k ⦌ B \in S)$
36		eleq1w	$⊢ k = i \to (k \in A \leftrightarrow i \in A)$
37	36	anbi2d	$⊢ k = i \to ((φ \land k \in A) \leftrightarrow (φ \land i \in A))$
38		csbeq1a	$⊢ k = i \to B = ⦋ i / k ⦌ B$
39	38	eleq1d	$⊢ k = i \to (B \in S \leftrightarrow ⦋ i / k ⦌ B \in S)$
40	37 39	imbi12d	$⊢ k = i \to (((φ \land k \in A) \to B \in S) \leftrightarrow ((φ \land i \in A) \to ⦋ i / k ⦌ B \in S))$
41	35 40 4	chvarfv	$⊢ (φ \land i \in A) \to ⦋ i / k ⦌ B \in S$
42	31 32 38 12	fvmptf	$⊢ (i \in A \land ⦋ i / k ⦌ B \in S) \to (k \in A ⟼ B) (i) = ⦋ i / k ⦌ B$
43	28 41 42	syl2anc	$⊢ (φ \land i \in A) \to (k \in A ⟼ B) (i) = ⦋ i / k ⦌ B$
44	43	disjeq2dv	$⊢ φ \to (\underset{i \in A}{Disj} (k \in A ⟼ B) (i) \leftrightarrow \underset{i \in A}{Disj} ⦋ i / k ⦌ B)$
45		nfcv	$⊢ \underline{Ⅎ} i B$
46	45 32 38	cbvdisj	$⊢ \underset{k \in A}{Disj} B \leftrightarrow \underset{i \in A}{Disj} ⦋ i / k ⦌ B$
47	46	bicomi	$⊢ \underset{i \in A}{Disj} ⦋ i / k ⦌ B \leftrightarrow \underset{k \in A}{Disj} B$
48	47	a1i	$⊢ φ \to (\underset{i \in A}{Disj} ⦋ i / k ⦌ B \leftrightarrow \underset{k \in A}{Disj} B)$
49	44 48	bitrd	$⊢ φ \to (\underset{i \in A}{Disj} (k \in A ⟼ B) (i) \leftrightarrow \underset{k \in A}{Disj} B)$
50	6 49	mpbird	$⊢ φ \to \underset{i \in A}{Disj} (k \in A ⟼ B) (i)$
51	2 3 23 24 27 50	meadjiunlem	$⊢ φ \to sum^({M ↾}_{ran (k \in A ⟼ B)}) = sum^(M \circ (k \in A ⟼ B))$
52	45 32 38	cbvmpt	$⊢ (k \in A ⟼ B) = (i \in A ⟼ ⦋ i / k ⦌ B)$
53	52	coeq2i	$⊢ M \circ (k \in A ⟼ B) = M \circ (i \in A ⟼ ⦋ i / k ⦌ B)$
54	53	a1i	$⊢ φ \to M \circ (k \in A ⟼ B) = M \circ (i \in A ⟼ ⦋ i / k ⦌ B)$
55		eqidd	$⊢ φ \to (i \in A ⟼ ⦋ i / k ⦌ B) = (i \in A ⟼ ⦋ i / k ⦌ B)$
56	2 3	meaf	$⊢ φ \to M : S ⟶ [0, +∞]$
57	56	feqmptd	$⊢ φ \to M = (y \in S ⟼ M (y))$
58		fveq2	$⊢ y = ⦋ i / k ⦌ B \to M (y) = M (⦋ i / k ⦌ B)$
59	41 55 57 58	fmptco	$⊢ φ \to M \circ (i \in A ⟼ ⦋ i / k ⦌ B) = (i \in A ⟼ M (⦋ i / k ⦌ B))$
60		nfcv	$⊢ \underline{Ⅎ} i M (B)$
61		nfcv	$⊢ \underline{Ⅎ} k M$
62	61 32	nffv	$⊢ \underline{Ⅎ} k M (⦋ i / k ⦌ B)$
63	38	fveq2d	$⊢ k = i \to M (B) = M (⦋ i / k ⦌ B)$
64	60 62 63	cbvmpt	$⊢ (k \in A ⟼ M (B)) = (i \in A ⟼ M (⦋ i / k ⦌ B))$
65	64	eqcomi	$⊢ (i \in A ⟼ M (⦋ i / k ⦌ B)) = (k \in A ⟼ M (B))$
66	65	a1i	$⊢ φ \to (i \in A ⟼ M (⦋ i / k ⦌ B)) = (k \in A ⟼ M (B))$
67	54 59 66	3eqtrd	$⊢ φ \to M \circ (k \in A ⟼ B) = (k \in A ⟼ M (B))$
68	67	fveq2d	$⊢ φ \to sum^(M \circ (k \in A ⟼ B)) = sum^((k \in A ⟼ M (B)))$
69	51 68	eqtrd	$⊢ φ \to sum^({M ↾}_{ran (k \in A ⟼ B)}) = sum^((k \in A ⟼ M (B)))$
70	11 19 69	3eqtrd	$⊢ φ \to M (⋃_{k \in A} B) = sum^((k \in A ⟼ M (B)))$

Metamath Proof Explorer

Theorem meadjiun

Proof