meadjuni

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	meadjuni.m	$⊢ φ \to M \in Meas$
	meadjuni.s	$⊢ S = dom M$
	meadjuni.x	$⊢ φ \to X \subseteq S$
	meadjuni.cnb	$⊢ φ \to X ≼ ω$
	meadjuni.dj	$⊢ φ \to \underset{x \in X}{Disj} x$
Assertion	meadjuni	$⊢ φ \to M (⋃ X) = sum^({M ↾}_{X})$

Proof

Step	Hyp	Ref	Expression
1		meadjuni.m	$⊢ φ \to M \in Meas$
2		meadjuni.s	$⊢ S = dom M$
3		meadjuni.x	$⊢ φ \to X \subseteq S$
4		meadjuni.cnb	$⊢ φ \to X ≼ ω$
5		meadjuni.dj	$⊢ φ \to \underset{x \in X}{Disj} x$
6		breq1	$⊢ y = X \to (y ≼ ω \leftrightarrow X ≼ ω)$
7		disjeq1	$⊢ y = X \to (\underset{x \in y}{Disj} x \leftrightarrow \underset{x \in X}{Disj} x)$
8	6 7	anbi12d	$⊢ y = X \to ((y ≼ ω \land \underset{x \in y}{Disj} x) \leftrightarrow (X ≼ ω \land \underset{x \in X}{Disj} x))$
9		unieq	$⊢ y = X \to ⋃ y = ⋃ X$
10	9	fveq2d	$⊢ y = X \to M (⋃ y) = M (⋃ X)$
11		reseq2	$⊢ y = X \to {M ↾}_{y} = {M ↾}_{X}$
12	11	fveq2d	$⊢ y = X \to sum^({M ↾}_{y}) = sum^({M ↾}_{X})$
13	10 12	eqeq12d	$⊢ y = X \to (M (⋃ y) = sum^({M ↾}_{y}) \leftrightarrow M (⋃ X) = sum^({M ↾}_{X}))$
14	8 13	imbi12d	$⊢ y = X \to (((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = sum^({M ↾}_{y})) \leftrightarrow ((X ≼ ω \land \underset{x \in X}{Disj} x) \to M (⋃ X) = sum^({M ↾}_{X})))$
15		ismea	$⊢ M \in Meas \leftrightarrow (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = sum^({M ↾}_{y})))$
16	1 15	sylib	$⊢ φ \to (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = sum^({M ↾}_{y})))$
17	16	simprd	$⊢ φ \to \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = sum^({M ↾}_{y}))$
18	1 2	dmmeasal	$⊢ φ \to S \in SAlg$
19	18 3	ssexd	$⊢ φ \to X \in V$
20	3 2	sseqtrdi	$⊢ φ \to X \subseteq dom M$
21	19 20	elpwd	$⊢ φ \to X \in 𝒫 dom M$
22	14 17 21	rspcdva	$⊢ φ \to ((X ≼ ω \land \underset{x \in X}{Disj} x) \to M (⋃ X) = sum^({M ↾}_{X}))$
23	4 5 22	mp2and	$⊢ φ \to M (⋃ X) = sum^({M ↾}_{X})$

Metamath Proof Explorer

Theorem meadjuni

Proof