measinblem

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

Proof

Step	Hyp	Ref	Expression
1		iunin1	$⊢ ⋃_{x \in B} (x \cap A) = ⋃_{x \in B} x \cap A$
2		uniiun	$⊢ ⋃ B = ⋃_{x \in B} x$
3	2	ineq1i	$⊢ ⋃ B \cap A = ⋃_{x \in B} x \cap A$
4	1 3	eqtr4i	$⊢ ⋃_{x \in B} (x \cap A) = ⋃ B \cap A$
5	4	fveq2i	$⊢ M (⋃_{x \in B} (x \cap A)) = M (⋃ B \cap A)$
6		simplll	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to M \in measures (S)$
7		nfv	$⊢ Ⅎ x ((M \in measures (S) \land A \in S) \land B \in 𝒫 S)$
8		nfv	$⊢ Ⅎ x B ≼ ω$
9		nfdisj1	$⊢ Ⅎ x \underset{x \in B}{Disj} x$
10	8 9	nfan	$⊢ Ⅎ x (B ≼ ω \land \underset{x \in B}{Disj} x)$
11	7 10	nfan	$⊢ Ⅎ x (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x))$
12		simp1ll	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to M \in measures (S)$
13		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
14	12 13	syl	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to S \in ⋃ ran sigAlgebra$
15		simp3	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to x \in B$
16		simp1r	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to B \in 𝒫 S$
17		elelpwi	$⊢ (x \in B \land B \in 𝒫 S) \to x \in S$
18	15 16 17	syl2anc	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to x \in S$
19		simp1lr	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to A \in S$
20		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land x \in S \land A \in S) \to x \cap A \in S$
21	14 18 19 20	syl3anc	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x) \land x \in B) \to x \cap A \in S$
22	21	3expia	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to (x \in B \to x \cap A \in S)$
23	11 22	ralrimi	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to \forall x \in B x \cap A \in S$
24		simprl	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to B ≼ ω$
25		disjin	$⊢ \underset{x \in B}{Disj} x \to \underset{x \in B}{Disj} (x \cap A)$
26	25	ad2antll	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to \underset{x \in B}{Disj} (x \cap A)$
27		measvuni	$⊢ (M \in measures (S) \land \forall x \in B x \cap A \in S \land (B ≼ ω \land \underset{x \in B}{Disj} (x \cap A))) \to M (⋃_{x \in B} (x \cap A)) = \underset{x \in B}{\sum^{*}} M (x \cap A)$
28	6 23 24 26 27	syl112anc	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to M (⋃_{x \in B} (x \cap A)) = \underset{x \in B}{\sum^{*}} M (x \cap A)$
29	5 28	eqtr3id	$⊢ (((M \in measures (S) \land A \in S) \land B \in 𝒫 S) \land (B ≼ ω \land \underset{x \in B}{Disj} x)) \to M (⋃ B \cap A) = \underset{x \in B}{\sum^{*}} M (x \cap A)$

Metamath Proof Explorer

Theorem measinblem

Proof