Theorem measinblem

Description: Lemma for measinb . (Contributed by Thierry Arnoux, 2-Jun-2017)

	Ref	Expression
Assertion	measinblem	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → ( 𝑀 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) = Σ* 𝑥 ∈ 𝐵 ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iunin1	⊢ ∪ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝑥 ∈ 𝐵 𝑥 ∩ 𝐴 )
2		uniiun	⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
3	2	ineq1i	⊢ ( ∪ 𝐵 ∩ 𝐴 ) = ( ∪ 𝑥 ∈ 𝐵 𝑥 ∩ 𝐴 )
4	1 3	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝐵 ∩ 𝐴 )
5	4	fveq2i	⊢ ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( ∪ 𝐵 ∩ 𝐴 ) )
6		simplll	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
7		nfv	⊢ Ⅎ 𝑥 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 )
8		nfv	⊢ Ⅎ 𝑥 𝐵 ≼ ω
9		nfdisj1	⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐵 𝑥
10	8 9	nfan	⊢ Ⅎ 𝑥 ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 )
11	7 10	nfan	⊢ Ⅎ 𝑥 ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) )
12		simp1ll	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
13		measbase	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
14	12 13	syl	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ ∪ ran sigAlgebra )
15		simp3	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
16		simp1r	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ 𝒫 𝑆 )
17		elelpwi	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝑆 ) → 𝑥 ∈ 𝑆 )
18	15 16 17	syl2anc	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑆 )
19		simp1lr	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑆 )
20		inelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
21	14 18 19 20	syl3anc	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
22	21	3expia	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) )
23	11 22	ralrimi	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
24		simprl	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → 𝐵 ≼ ω )
25		disjin	⊢ ( Disj 𝑥 ∈ 𝐵 𝑥 → Disj 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) )
26	25	ad2antll	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → Disj 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) )
27		measvuni	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ) = Σ* 𝑥 ∈ 𝐵 ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
28	6 23 24 26 27	syl112anc	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐵 ( 𝑥 ∩ 𝐴 ) ) = Σ* 𝑥 ∈ 𝐵 ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
29	5 28	eqtr3id	⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝒫 𝑆 ) ∧ ( 𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥 ) ) → ( 𝑀 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) = Σ* 𝑥 ∈ 𝐵 ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )