pmeasadd

Description: A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Hypotheses	caraext.1	$⊢ φ \to P : R ⟶ [0, +∞]$
	caraext.2	$⊢ φ \to P (\emptyset) = 0$
	caraext.3	$⊢ (φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{*}} P (y)$
	pmeassubadd.q	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
	pmeassubadd.1	$⊢ φ \to R \in Q$
	pmeassubadd.2	$⊢ φ \to A ≼ ω$
	pmeassubadd.3	$⊢ (φ \land k \in A) \to B \in R$
	pmeasadd.4	$⊢ φ \to \underset{k \in A}{Disj} B$
Assertion	pmeasadd	$⊢ φ \to P (⋃_{k \in A} B) = \underset{k \in A}{\sum^{*}} P (B)$

Proof

Step	Hyp	Ref	Expression
1		caraext.1	$⊢ φ \to P : R ⟶ [0, +∞]$
2		caraext.2	$⊢ φ \to P (\emptyset) = 0$
3		caraext.3	$⊢ (φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{*}} P (y)$
4		pmeassubadd.q	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
5		pmeassubadd.1	$⊢ φ \to R \in Q$
6		pmeassubadd.2	$⊢ φ \to A ≼ ω$
7		pmeassubadd.3	$⊢ (φ \land k \in A) \to B \in R$
8		pmeasadd.4	$⊢ φ \to \underset{k \in A}{Disj} B$
9	7	ralrimiva	$⊢ φ \to \forall k \in A B \in R$
10		dfiun3g	$⊢ \forall k \in A B \in R \to ⋃_{k \in A} B = ⋃ ran (k \in A ⟼ B)$
11	9 10	syl	$⊢ φ \to ⋃_{k \in A} B = ⋃ ran (k \in A ⟼ B)$
12	11	fveq2d	$⊢ φ \to P (⋃_{k \in A} B) = P (⋃ ran (k \in A ⟼ B))$
13		mptct	$⊢ A ≼ ω \to (k \in A ⟼ B) ≼ ω$
14		rnct	$⊢ (k \in A ⟼ B) ≼ ω \to ran (k \in A ⟼ B) ≼ ω$
15	6 13 14	3syl	$⊢ φ \to ran (k \in A ⟼ B) ≼ ω$
16		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
17	16	rnmptss	$⊢ \forall k \in A B \in R \to ran (k \in A ⟼ B) \subseteq R$
18	9 17	syl	$⊢ φ \to ran (k \in A ⟼ B) \subseteq R$
19		disjrnmpt	$⊢ \underset{k \in A}{Disj} B \to \underset{y \in ran (k \in A ⟼ B)}{Disj} y$
20	8 19	syl	$⊢ φ \to \underset{y \in ran (k \in A ⟼ B)}{Disj} y$
21	15 18 20	3jca	$⊢ φ \to (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y)$
22	21	ancli	$⊢ φ \to (φ \land (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y))$
23		ctex	$⊢ A ≼ ω \to A \in V$
24		mptexg	$⊢ A \in V \to (k \in A ⟼ B) \in V$
25	6 23 24	3syl	$⊢ φ \to (k \in A ⟼ B) \in V$
26		rnexg	$⊢ (k \in A ⟼ B) \in V \to ran (k \in A ⟼ B) \in V$
27		breq1	$⊢ x = ran (k \in A ⟼ B) \to (x ≼ ω \leftrightarrow ran (k \in A ⟼ B) ≼ ω)$
28		sseq1	$⊢ x = ran (k \in A ⟼ B) \to (x \subseteq R \leftrightarrow ran (k \in A ⟼ B) \subseteq R)$
29		disjeq1	$⊢ x = ran (k \in A ⟼ B) \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in ran (k \in A ⟼ B)}{Disj} y)$
30	27 28 29	3anbi123d	$⊢ x = ran (k \in A ⟼ B) \to ((x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y) \leftrightarrow (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y))$
31	30	anbi2d	$⊢ x = ran (k \in A ⟼ B) \to ((φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \leftrightarrow (φ \land (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y)))$
32		unieq	$⊢ x = ran (k \in A ⟼ B) \to ⋃ x = ⋃ ran (k \in A ⟼ B)$
33	32	fveq2d	$⊢ x = ran (k \in A ⟼ B) \to P (⋃ x) = P (⋃ ran (k \in A ⟼ B))$
34		esumeq1	$⊢ x = ran (k \in A ⟼ B) \to \underset{y \in x}{\sum^{}} P (y) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} P (y)$
35	33 34	eqeq12d	$⊢ x = ran (k \in A ⟼ B) \to (P (⋃ x) = \underset{y \in x}{\sum^{}} P (y) \leftrightarrow P (⋃ ran (k \in A ⟼ B)) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} P (y))$
36	31 35	imbi12d	$⊢ x = ran (k \in A ⟼ B) \to (((φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{}} P (y)) \leftrightarrow ((φ \land (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y)) \to P (⋃ ran (k \in A ⟼ B)) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} P (y)))$
37	36 3	vtoclg	$⊢ ran (k \in A ⟼ B) \in V \to ((φ \land (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y)) \to P (⋃ ran (k \in A ⟼ B)) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{*}} P (y))$
38	25 26 37	3syl	$⊢ φ \to ((φ \land (ran (k \in A ⟼ B) ≼ ω \land ran (k \in A ⟼ B) \subseteq R \land \underset{y \in ran (k \in A ⟼ B)}{Disj} y)) \to P (⋃ ran (k \in A ⟼ B)) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{*}} P (y))$
39	22 38	mpd	$⊢ φ \to P (⋃ ran (k \in A ⟼ B)) = \underset{y \in ran (k \in A ⟼ B)}{\sum^{*}} P (y)$
40		fveq2	$⊢ y = B \to P (y) = P (B)$
41	6 23	syl	$⊢ φ \to A \in V$
42	1	adantr	$⊢ (φ \land k \in A) \to P : R ⟶ [0, +∞]$
43	42 7	ffvelrnd	$⊢ (φ \land k \in A) \to P (B) \in [0, +∞]$
44		fveq2	$⊢ B = \emptyset \to P (B) = P (\emptyset)$
45	44	adantl	$⊢ ((φ \land k \in A) \land B = \emptyset) \to P (B) = P (\emptyset)$
46	2	ad2antrr	$⊢ ((φ \land k \in A) \land B = \emptyset) \to P (\emptyset) = 0$
47	45 46	eqtrd	$⊢ ((φ \land k \in A) \land B = \emptyset) \to P (B) = 0$
48	40 41 43 7 47 8	esumrnmpt2	$⊢ φ \to \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} P (y) = \underset{k \in A}{\sum^{}} P (B)$
49	12 39 48	3eqtrd	$⊢ φ \to P (⋃_{k \in A} B) = \underset{k \in A}{\sum^{*}} P (B)$

Metamath Proof Explorer

Theorem pmeasadd

Proof