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 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → 𝐴 ∈ 𝒫 𝑆 )
2 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
3 ismeas ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) )
4 2 3 syl ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) )
5 4 ibi ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) )
6 5 simp3d ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) )
7 6 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) )
8 simp3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) )
9 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≼ ω ↔ 𝐴 ≼ ω ) )
10 disjeq1 ⊢ ( 𝑦 = 𝐴 → ( Disj 𝑥 ∈ 𝑦 𝑥 ↔ Disj 𝑥 ∈ 𝐴 𝑥 ) )
11 9 10 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) ↔ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) )
12 unieq ⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = ∪ 𝐴 )
13 12 fveq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑀 ‘ ∪ 𝑦 ) = ( 𝑀 ‘ ∪ 𝐴 ) )
14 esumeq1 ⊢ ( 𝑦 = 𝐴 → Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) )
15 13 14 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ↔ ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) )
16 11 15 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ↔ ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) ) )
17 16 rspcv ⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) → ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) ) )
18 1 7 8 17 syl3c ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) )