Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meadjuni.s	⊢ 𝑆 = dom 𝑀
	meadjuni.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
	meadjuni.cnb	⊢ ( 𝜑 → 𝑋 ≼ ω )
	meadjuni.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝑥 )
Assertion	meadjuni	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑋 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meadjuni.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meadjuni.s	⊢ 𝑆 = dom 𝑀
3		meadjuni.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
4		meadjuni.cnb	⊢ ( 𝜑 → 𝑋 ≼ ω )
5		meadjuni.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝑥 )
6		breq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ≼ ω ↔ 𝑋 ≼ ω ) )
7		disjeq1	⊢ ( 𝑦 = 𝑋 → ( Disj 𝑥 ∈ 𝑦 𝑥 ↔ Disj 𝑥 ∈ 𝑋 𝑥 ) )
8	6 7	anbi12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) ↔ ( 𝑋 ≼ ω ∧ Disj 𝑥 ∈ 𝑋 𝑥 ) ) )
9		unieq	⊢ ( 𝑦 = 𝑋 → ∪ 𝑦 = ∪ 𝑋 )
10	9	fveq2d	⊢ ( 𝑦 = 𝑋 → ( 𝑀 ‘ ∪ 𝑦 ) = ( 𝑀 ‘ ∪ 𝑋 ) )
11		reseq2	⊢ ( 𝑦 = 𝑋 → ( 𝑀 ↾ 𝑦 ) = ( 𝑀 ↾ 𝑋 ) )
12	11	fveq2d	⊢ ( 𝑦 = 𝑋 → ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) )
13	10 12	eqeq12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ↔ ( 𝑀 ‘ ∪ 𝑋 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) ) )
14	8 13	imbi12d	⊢ ( 𝑦 = 𝑋 → ( ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ↔ ( ( 𝑋 ≼ ω ∧ Disj 𝑥 ∈ 𝑋 𝑥 ) → ( 𝑀 ‘ ∪ 𝑋 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) ) ) )
15		ismea	⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
16	1 15	sylib	⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
17	16	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
18	1 2	dmmeasal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
19	18 3	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
20	3 2	sseqtrdi	⊢ ( 𝜑 → 𝑋 ⊆ dom 𝑀 )
21	19 20	elpwd	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 dom 𝑀 )
22	14 17 21	rspcdva	⊢ ( 𝜑 → ( ( 𝑋 ≼ ω ∧ Disj 𝑥 ∈ 𝑋 𝑥 ) → ( 𝑀 ‘ ∪ 𝑋 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) ) )
23	4 5 22	mp2and	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑋 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑋 ) ) )