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 ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∧ A ≼ ω ∧ Disj x ∈ A B → M ⁡ ⋃ x ∈ A B = ∑ * x ∈ A M ⁡ B

Proof

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