Metamath Proof Explorer

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 
|- ( ph -> M e. Meas )
meadjuni.s 
|- S = dom M
meadjuni.x 
|- ( ph -> X C_ S )
meadjuni.cnb 
|- ( ph -> X ~<_ _om )
meadjuni.dj 
|- ( ph -> Disj_ x e. X x )
Assertion meadjuni 
|- ( ph -> ( M ` U. X ) = ( sum^ ` ( M |` X ) ) )

Proof

Step Hyp Ref Expression
1 meadjuni.m 
 |-  ( ph -> M e. Meas )
2 meadjuni.s 
 |-  S = dom M
3 meadjuni.x 
 |-  ( ph -> X C_ S )
4 meadjuni.cnb 
 |-  ( ph -> X ~<_ _om )
5 meadjuni.dj 
 |-  ( ph -> Disj_ x e. X x )
6 breq1 
 |-  ( y = X -> ( y ~<_ _om <-> X ~<_ _om ) )
7 disjeq1 
 |-  ( y = X -> ( Disj_ x e. y x <-> Disj_ x e. X x ) )
8 6 7 anbi12d 
 |-  ( y = X -> ( ( y ~<_ _om /\ Disj_ x e. y x ) <-> ( X ~<_ _om /\ Disj_ x e. X x ) ) )
9 unieq 
 |-  ( y = X -> U. y = U. X )
10 9 fveq2d 
 |-  ( y = X -> ( M ` U. y ) = ( M ` U. X ) )
11 reseq2 
 |-  ( y = X -> ( M |` y ) = ( M |` X ) )
12 11 fveq2d 
 |-  ( y = X -> ( sum^ ` ( M |` y ) ) = ( sum^ ` ( M |` X ) ) )
13 10 12 eqeq12d 
 |-  ( y = X -> ( ( M ` U. y ) = ( sum^ ` ( M |` y ) ) <-> ( M ` U. X ) = ( sum^ ` ( M |` X ) ) ) )
14 8 13 imbi12d 
 |-  ( y = X -> ( ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) <-> ( ( X ~<_ _om /\ Disj_ x e. X x ) -> ( M ` U. X ) = ( sum^ ` ( M |` X ) ) ) ) )
15 ismea 
 |-  ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) ) )
16 1 15 sylib 
 |-  ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) ) )
17 16 simprd 
 |-  ( ph -> A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) )
18 1 2 dmmeasal 
 |-  ( ph -> S e. SAlg )
19 18 3 ssexd 
 |-  ( ph -> X e. _V )
20 3 2 sseqtrdi 
 |-  ( ph -> X C_ dom M )
21 19 20 elpwd 
 |-  ( ph -> X e. ~P dom M )
22 14 17 21 rspcdva 
 |-  ( ph -> ( ( X ~<_ _om /\ Disj_ x e. X x ) -> ( M ` U. X ) = ( sum^ ` ( M |` X ) ) ) )
23 4 5 22 mp2and 
 |-  ( ph -> ( M ` U. X ) = ( sum^ ` ( M |` X ) ) )