Metamath Proof Explorer

Theorem measvuni

Description: The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of S . (Contributed by Thierry Arnoux, 7-Mar-2017)

Ref Expression
Assertion measvuni 
|- ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> M e. ( measures ` S ) )
2 rabid 
 |-  ( x e. { x e. A | B e. { (/) } } <-> ( x e. A /\ B e. { (/) } ) )
3 2 simprbi 
 |-  ( x e. { x e. A | B e. { (/) } } -> B e. { (/) } )
4 3 adantl 
 |-  ( ( M e. ( measures ` S ) /\ x e. { x e. A | B e. { (/) } } ) -> B e. { (/) } )
5 4 ralrimiva 
 |-  ( M e. ( measures ` S ) -> A. x e. { x e. A | B e. { (/) } } B e. { (/) } )
6 5 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. { x e. A | B e. { (/) } } B e. { (/) } )
7 ssrab2 
 |-  { x e. A | B e. { (/) } } C_ A
8 ssct 
 |-  ( ( { x e. A | B e. { (/) } } C_ A /\ A ~<_ _om ) -> { x e. A | B e. { (/) } } ~<_ _om )
9 7 8 mpan 
 |-  ( A ~<_ _om -> { x e. A | B e. { (/) } } ~<_ _om )
10 9 adantr 
 |-  ( ( A ~<_ _om /\ Disj_ x e. A B ) -> { x e. A | B e. { (/) } } ~<_ _om )
11 10 3ad2ant3 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { x e. A | B e. { (/) } } ~<_ _om )
12 simp3r 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Disj_ x e. A B )
13 nfrab1 
 |-  F/_ x { x e. A | B e. { (/) } }
14 nfcv 
 |-  F/_ x A
15 13 14 disjss1f 
 |-  ( { x e. A | B e. { (/) } } C_ A -> ( Disj_ x e. A B -> Disj_ x e. { x e. A | B e. { (/) } } B ) )
16 7 12 15 mpsyl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Disj_ x e. { x e. A | B e. { (/) } } B )
17 13 measvunilem0 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. { x e. A | B e. { (/) } } B e. { (/) } /\ ( { x e. A | B e. { (/) } } ~<_ _om /\ Disj_ x e. { x e. A | B e. { (/) } } B ) ) -> ( M ` U_ x e. { x e. A | B e. { (/) } } B ) = sum* x e. { x e. A | B e. { (/) } } ( M ` B ) )
18 1 6 11 16 17 syl112anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. { x e. A | B e. { (/) } } B ) = sum* x e. { x e. A | B e. { (/) } } ( M ` B ) )
19 rabid 
 |-  ( x e. { x e. A | B e. ( S \ { (/) } ) } <-> ( x e. A /\ B e. ( S \ { (/) } ) ) )
20 19 simprbi 
 |-  ( x e. { x e. A | B e. ( S \ { (/) } ) } -> B e. ( S \ { (/) } ) )
21 20 adantl 
 |-  ( ( M e. ( measures ` S ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> B e. ( S \ { (/) } ) )
22 21 ralrimiva 
 |-  ( M e. ( measures ` S ) -> A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. ( S \ { (/) } ) )
23 22 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. ( S \ { (/) } ) )
24 ssrab2 
 |-  { x e. A | B e. ( S \ { (/) } ) } C_ A
25 ssct 
 |-  ( ( { x e. A | B e. ( S \ { (/) } ) } C_ A /\ A ~<_ _om ) -> { x e. A | B e. ( S \ { (/) } ) } ~<_ _om )
26 24 25 mpan 
 |-  ( A ~<_ _om -> { x e. A | B e. ( S \ { (/) } ) } ~<_ _om )
27 26 adantr 
 |-  ( ( A ~<_ _om /\ Disj_ x e. A B ) -> { x e. A | B e. ( S \ { (/) } ) } ~<_ _om )
28 27 3ad2ant3 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { x e. A | B e. ( S \ { (/) } ) } ~<_ _om )
29 nfrab1 
 |-  F/_ x { x e. A | B e. ( S \ { (/) } ) }
30 29 14 disjss1f 
 |-  ( { x e. A | B e. ( S \ { (/) } ) } C_ A -> ( Disj_ x e. A B -> Disj_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) )
31 24 12 30 mpsyl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Disj_ x e. { x e. A | B e. ( S \ { (/) } ) } B )
32 29 measvunilem 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. ( S \ { (/) } ) /\ ( { x e. A | B e. ( S \ { (/) } ) } ~<_ _om /\ Disj_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) -> ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = sum* x e. { x e. A | B e. ( S \ { (/) } ) } ( M ` B ) )
33 1 23 28 31 32 syl112anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = sum* x e. { x e. A | B e. ( S \ { (/) } ) } ( M ` B ) )
34 18 33 oveq12d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( ( M ` U_ x e. { x e. A | B e. { (/) } } B ) +e ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) = ( sum* x e. { x e. A | B e. { (/) } } ( M ` B ) +e sum* x e. { x e. A | B e. ( S \ { (/) } ) } ( M ` B ) ) )
35 nfv 
 |-  F/ x M e. ( measures ` S )
36 nfra1 
 |-  F/ x A. x e. A B e. S
37 nfv 
 |-  F/ x A ~<_ _om
38 nfdisj1 
 |-  F/ x Disj_ x e. A B
39 37 38 nfan 
 |-  F/ x ( A ~<_ _om /\ Disj_ x e. A B )
40 35 36 39 nf3an 
 |-  F/ x ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) )
41 13 29 nfun 
 |-  F/_ x ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } )
42 simp2 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. A B e. S )
43 rabid2 
 |-  ( A = { x e. A | B e. S } <-> A. x e. A B e. S )
44 42 43 sylibr 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A = { x e. A | B e. S } )
45 elun 
 |-  ( B e. ( { (/) } u. ( S \ { (/) } ) ) <-> ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) )
46 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
47 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
48 snssi 
 |-  ( (/) e. S -> { (/) } C_ S )
49 46 47 48 3syl 
 |-  ( M e. ( measures ` S ) -> { (/) } C_ S )
50 undif 
 |-  ( { (/) } C_ S <-> ( { (/) } u. ( S \ { (/) } ) ) = S )
51 49 50 sylib 
 |-  ( M e. ( measures ` S ) -> ( { (/) } u. ( S \ { (/) } ) ) = S )
52 51 eleq2d 
 |-  ( M e. ( measures ` S ) -> ( B e. ( { (/) } u. ( S \ { (/) } ) ) <-> B e. S ) )
53 45 52 bitr3id 
 |-  ( M e. ( measures ` S ) -> ( ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) <-> B e. S ) )
54 53 rabbidv 
 |-  ( M e. ( measures ` S ) -> { x e. A | ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) } = { x e. A | B e. S } )
55 54 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { x e. A | ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) } = { x e. A | B e. S } )
56 44 55 eqtr4d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A = { x e. A | ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) } )
57 unrab 
 |-  ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) = { x e. A | ( B e. { (/) } \/ B e. ( S \ { (/) } ) ) }
58 56 57 eqtr4di 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A = ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) )
59 eqidd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> B = B )
60 40 14 41 58 59 iuneq12df 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> U_ x e. A B = U_ x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) B )
61 60 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = ( M ` U_ x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) B ) )
62 iunxun 
 |-  U_ x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) B = ( U_ x e. { x e. A | B e. { (/) } } B u. U_ x e. { x e. A | B e. ( S \ { (/) } ) } B )
63 62 fveq2i 
 |-  ( M ` U_ x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) B ) = ( M ` ( U_ x e. { x e. A | B e. { (/) } } B u. U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) )
64 61 63 eqtrdi 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = ( M ` ( U_ x e. { x e. A | B e. { (/) } } B u. U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) )
65 46 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> S e. U. ran sigAlgebra )
66 47 adantr 
 |-  ( ( S e. U. ran sigAlgebra /\ B e. { (/) } ) -> (/) e. S )
67 elsni 
 |-  ( B e. { (/) } -> B = (/) )
68 67 eleq1d 
 |-  ( B e. { (/) } -> ( B e. S <-> (/) e. S ) )
69 68 adantl 
 |-  ( ( S e. U. ran sigAlgebra /\ B e. { (/) } ) -> ( B e. S <-> (/) e. S ) )
70 66 69 mpbird 
 |-  ( ( S e. U. ran sigAlgebra /\ B e. { (/) } ) -> B e. S )
71 46 3 70 syl2an 
 |-  ( ( M e. ( measures ` S ) /\ x e. { x e. A | B e. { (/) } } ) -> B e. S )
72 71 ralrimiva 
 |-  ( M e. ( measures ` S ) -> A. x e. { x e. A | B e. { (/) } } B e. S )
73 72 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. { x e. A | B e. { (/) } } B e. S )
74 13 sigaclcuni 
 |-  ( ( S e. U. ran sigAlgebra /\ A. x e. { x e. A | B e. { (/) } } B e. S /\ { x e. A | B e. { (/) } } ~<_ _om ) -> U_ x e. { x e. A | B e. { (/) } } B e. S )
75 65 73 11 74 syl3anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> U_ x e. { x e. A | B e. { (/) } } B e. S )
76 21 eldifad 
 |-  ( ( M e. ( measures ` S ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> B e. S )
77 76 ralrimiva 
 |-  ( M e. ( measures ` S ) -> A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. S )
78 77 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. S )
79 29 sigaclcuni 
 |-  ( ( S e. U. ran sigAlgebra /\ A. x e. { x e. A | B e. ( S \ { (/) } ) } B e. S /\ { x e. A | B e. ( S \ { (/) } ) } ~<_ _om ) -> U_ x e. { x e. A | B e. ( S \ { (/) } ) } B e. S )
80 65 78 28 79 syl3anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> U_ x e. { x e. A | B e. ( S \ { (/) } ) } B e. S )
81 3 67 syl 
 |-  ( x e. { x e. A | B e. { (/) } } -> B = (/) )
82 81 iuneq2i 
 |-  U_ x e. { x e. A | B e. { (/) } } B = U_ x e. { x e. A | B e. { (/) } } (/)
83 iun0 
 |-  U_ x e. { x e. A | B e. { (/) } } (/) = (/)
84 82 83 eqtri 
 |-  U_ x e. { x e. A | B e. { (/) } } B = (/)
85 ineq1 
 |-  ( U_ x e. { x e. A | B e. { (/) } } B = (/) -> ( U_ x e. { x e. A | B e. { (/) } } B i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = ( (/) i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) )
86 0in 
 |-  ( (/) i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = (/)
87 85 86 eqtrdi 
 |-  ( U_ x e. { x e. A | B e. { (/) } } B = (/) -> ( U_ x e. { x e. A | B e. { (/) } } B i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = (/) )
88 84 87 mp1i 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( U_ x e. { x e. A | B e. { (/) } } B i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = (/) )
89 measun 
 |-  ( ( M e. ( measures ` S ) /\ ( U_ x e. { x e. A | B e. { (/) } } B e. S /\ U_ x e. { x e. A | B e. ( S \ { (/) } ) } B e. S ) /\ ( U_ x e. { x e. A | B e. { (/) } } B i^i U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) = (/) ) -> ( M ` ( U_ x e. { x e. A | B e. { (/) } } B u. U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) = ( ( M ` U_ x e. { x e. A | B e. { (/) } } B ) +e ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) )
90 1 75 80 88 89 syl121anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` ( U_ x e. { x e. A | B e. { (/) } } B u. U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) = ( ( M ` U_ x e. { x e. A | B e. { (/) } } B ) +e ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) )
91 64 90 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = ( ( M ` U_ x e. { x e. A | B e. { (/) } } B ) +e ( M ` U_ x e. { x e. A | B e. ( S \ { (/) } ) } B ) ) )
92 40 58 esumeq1d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. A ( M ` B ) = sum* x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) ( M ` B ) )
93 ctex 
 |-  ( { x e. A | B e. { (/) } } ~<_ _om -> { x e. A | B e. { (/) } } e. _V )
94 11 93 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { x e. A | B e. { (/) } } e. _V )
95 ctex 
 |-  ( { x e. A | B e. ( S \ { (/) } ) } ~<_ _om -> { x e. A | B e. ( S \ { (/) } ) } e. _V )
96 28 95 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { x e. A | B e. ( S \ { (/) } ) } e. _V )
97 inrab 
 |-  ( { x e. A | B e. { (/) } } i^i { x e. A | B e. ( S \ { (/) } ) } ) = { x e. A | ( B e. { (/) } /\ B e. ( S \ { (/) } ) ) }
98 noel 
 |-  -. B e. (/)
99 disjdif 
 |-  ( { (/) } i^i ( S \ { (/) } ) ) = (/)
100 99 eleq2i 
 |-  ( B e. ( { (/) } i^i ( S \ { (/) } ) ) <-> B e. (/) )
101 98 100 mtbir 
 |-  -. B e. ( { (/) } i^i ( S \ { (/) } ) )
102 elin 
 |-  ( B e. ( { (/) } i^i ( S \ { (/) } ) ) <-> ( B e. { (/) } /\ B e. ( S \ { (/) } ) ) )
103 101 102 mtbi 
 |-  -. ( B e. { (/) } /\ B e. ( S \ { (/) } ) )
104 103 rgenw 
 |-  A. x e. A -. ( B e. { (/) } /\ B e. ( S \ { (/) } ) )
105 rabeq0 
 |-  ( { x e. A | ( B e. { (/) } /\ B e. ( S \ { (/) } ) ) } = (/) <-> A. x e. A -. ( B e. { (/) } /\ B e. ( S \ { (/) } ) ) )
106 104 105 mpbir 
 |-  { x e. A | ( B e. { (/) } /\ B e. ( S \ { (/) } ) ) } = (/)
107 97 106 eqtri 
 |-  ( { x e. A | B e. { (/) } } i^i { x e. A | B e. ( S \ { (/) } ) } ) = (/)
108 107 a1i 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( { x e. A | B e. { (/) } } i^i { x e. A | B e. ( S \ { (/) } ) } ) = (/) )
109 1 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. { (/) } } ) -> M e. ( measures ` S ) )
110 1 71 sylan 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. { (/) } } ) -> B e. S )
111 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. ( 0 [,] +oo ) )
112 109 110 111 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. { (/) } } ) -> ( M ` B ) e. ( 0 [,] +oo ) )
113 1 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> M e. ( measures ` S ) )
114 20 adantl 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> B e. ( S \ { (/) } ) )
115 114 eldifad 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> B e. S )
116 113 115 111 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. { x e. A | B e. ( S \ { (/) } ) } ) -> ( M ` B ) e. ( 0 [,] +oo ) )
117 40 13 29 94 96 108 112 116 esumsplit 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. ( { x e. A | B e. { (/) } } u. { x e. A | B e. ( S \ { (/) } ) } ) ( M ` B ) = ( sum* x e. { x e. A | B e. { (/) } } ( M ` B ) +e sum* x e. { x e. A | B e. ( S \ { (/) } ) } ( M ` B ) ) )
118 92 117 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. A ( M ` B ) = ( sum* x e. { x e. A | B e. { (/) } } ( M ` B ) +e sum* x e. { x e. A | B e. ( S \ { (/) } ) } ( M ` B ) ) )
119 34 91 118 3eqtr4d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )