Metamath Proof Explorer

Theorem measvun

Description: The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016)

		Ref	Expression
	Assertion	measvun	$⊢ (M \in measures (S) \land A \in 𝒫 S \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to M (⋃ A) = \underset{x \in A}{\sum^{*}} M (x)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (M \in measures (S) \land A \in 𝒫 S \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to A \in 𝒫 S$
2		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
3		ismeas	$⊢ S \in ⋃ ran sigAlgebra \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{*}} M (x))))$
4	2 3	syl	$⊢ M \in measures (S) \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{*}} M (x))))$
5	4	ibi	$⊢ M \in measures (S) \to (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{*}} M (x)))$
6	5	simp3d	$⊢ M \in measures (S) \to \forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{*}} M (x))$
7	6	3ad2ant1	$⊢ (M \in measures (S) \land A \in 𝒫 S \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to \forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{*}} M (x))$
8		simp3	$⊢ (M \in measures (S) \land A \in 𝒫 S \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to (A ≼ ω \land \underset{x \in A}{Disj} x)$
9		breq1	$⊢ y = A \to (y ≼ ω \leftrightarrow A ≼ ω)$
10		disjeq1	$⊢ y = A \to (\underset{x \in y}{Disj} x \leftrightarrow \underset{x \in A}{Disj} x)$
11	9 10	anbi12d	$⊢ y = A \to ((y ≼ ω \land \underset{x \in y}{Disj} x) \leftrightarrow (A ≼ ω \land \underset{x \in A}{Disj} x))$
12		unieq	$⊢ y = A \to ⋃ y = ⋃ A$
13	12	fveq2d	$⊢ y = A \to M (⋃ y) = M (⋃ A)$
14		esumeq1	$⊢ y = A \to \underset{x \in y}{\sum^{}} M (x) = \underset{x \in A}{\sum^{}} M (x)$
15	13 14	eqeq12d	$⊢ y = A \to (M (⋃ y) = \underset{x \in y}{\sum^{}} M (x) \leftrightarrow M (⋃ A) = \underset{x \in A}{\sum^{}} M (x))$
16	11 15	imbi12d	$⊢ y = A \to (((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{}} M (x)) \leftrightarrow ((A ≼ ω \land \underset{x \in A}{Disj} x) \to M (⋃ A) = \underset{x \in A}{\sum^{}} M (x)))$
17	16	rspcv	$⊢ A \in 𝒫 S \to (\forall y \in 𝒫 S ((y ≼ ω \land \underset{x \in y}{Disj} x) \to M (⋃ y) = \underset{x \in y}{\sum^{}} M (x)) \to ((A ≼ ω \land \underset{x \in A}{Disj} x) \to M (⋃ A) = \underset{x \in A}{\sum^{}} M (x)))$
18	1 7 8 17	syl3c	$⊢ (M \in measures (S) \land A \in 𝒫 S \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to M (⋃ A) = \underset{x \in A}{\sum^{*}} M (x)$