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

Metamath Proof Explorer

Theorem meadjiun

Proof