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 e. ( measures ` S ) /\ A e. ~P S /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( M ` U. A ) = sum* x e. A ( M ` x ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( M e. ( measures ` S ) /\ A e. ~P S /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> A e. ~P S )
2 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
3 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( M e. ( measures ` S ) <-> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) ) )
4 2 3 syl 
 |-  ( M e. ( measures ` S ) -> ( M e. ( measures ` S ) <-> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) ) )
5 4 ibi 
 |-  ( M e. ( measures ` S ) -> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) )
6 5 simp3d 
 |-  ( M e. ( measures ` S ) -> A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) )
7 6 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A e. ~P S /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) )
8 simp3 
 |-  ( ( M e. ( measures ` S ) /\ A e. ~P S /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( A ~<_ _om /\ Disj_ x e. A x ) )
9 breq1 
 |-  ( y = A -> ( y ~<_ _om <-> A ~<_ _om ) )
10 disjeq1 
 |-  ( y = A -> ( Disj_ x e. y x <-> Disj_ x e. A x ) )
11 9 10 anbi12d 
 |-  ( y = A -> ( ( y ~<_ _om /\ Disj_ x e. y x ) <-> ( A ~<_ _om /\ Disj_ x e. A x ) ) )
12 unieq 
 |-  ( y = A -> U. y = U. A )
13 12 fveq2d 
 |-  ( y = A -> ( M ` U. y ) = ( M ` U. A ) )
14 esumeq1 
 |-  ( y = A -> sum* x e. y ( M ` x ) = sum* x e. A ( M ` x ) )
15 13 14 eqeq12d 
 |-  ( y = A -> ( ( M ` U. y ) = sum* x e. y ( M ` x ) <-> ( M ` U. A ) = sum* x e. A ( M ` x ) ) )
16 11 15 imbi12d 
 |-  ( y = A -> ( ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) <-> ( ( A ~<_ _om /\ Disj_ x e. A x ) -> ( M ` U. A ) = sum* x e. A ( M ` x ) ) ) )
17 16 rspcv 
 |-  ( A e. ~P S -> ( A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) -> ( ( A ~<_ _om /\ Disj_ x e. A x ) -> ( M ` U. A ) = sum* x e. A ( M ` x ) ) ) )
18 1 7 8 17 syl3c 
 |-  ( ( M e. ( measures ` S ) /\ A e. ~P S /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( M ` U. A ) = sum* x e. A ( M ` x ) )