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 syl5bbr 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 syl6eqr 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 syl6eq 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 syl6eq 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