Metamath Proof Explorer


Theorem measiuns

Description: The measure of the union of a collection of sets, expressed as the sum of a disjoint set. This is used as a lemma for both measiun and meascnbl . (Contributed by Thierry Arnoux, 22-Jan-2017) (Proof shortened by Thierry Arnoux, 7-Feb-2017)

Ref Expression
Hypotheses measiuns.0 _ n B
measiuns.1 n = k A = B
measiuns.2 φ N = N = 1 ..^ I
measiuns.3 φ M measures S
measiuns.4 φ n N A S
Assertion measiuns φ M n N A = * n N M A k 1 ..^ n B

Proof

Step Hyp Ref Expression
1 measiuns.0 _ n B
2 measiuns.1 n = k A = B
3 measiuns.2 φ N = N = 1 ..^ I
4 measiuns.3 φ M measures S
5 measiuns.4 φ n N A S
6 1 2 3 iundisjcnt φ n N A = n N A k 1 ..^ n B
7 6 fveq2d φ M n N A = M n N A k 1 ..^ n B
8 measbase M measures S S ran sigAlgebra
9 4 8 syl φ S ran sigAlgebra
10 9 adantr φ n N S ran sigAlgebra
11 simpll φ n N k 1 ..^ n φ
12 fzossnn 1 ..^ n
13 simpr φ n N N = N =
14 12 13 sseqtrrid φ n N N = 1 ..^ n N
15 simplr φ n N N = 1 ..^ I n N
16 simpr φ n N N = 1 ..^ I N = 1 ..^ I
17 15 16 eleqtrd φ n N N = 1 ..^ I n 1 ..^ I
18 elfzouz2 n 1 ..^ I I n
19 fzoss2 I n 1 ..^ n 1 ..^ I
20 17 18 19 3syl φ n N N = 1 ..^ I 1 ..^ n 1 ..^ I
21 20 16 sseqtrrd φ n N N = 1 ..^ I 1 ..^ n N
22 3 adantr φ n N N = N = 1 ..^ I
23 14 21 22 mpjaodan φ n N 1 ..^ n N
24 23 sselda φ n N k 1 ..^ n k N
25 5 sbimi k n φ n N k n A S
26 sban k n φ n N k n φ k n n N
27 sbv k n φ φ
28 clelsb3 k n n N k N
29 27 28 anbi12i k n φ k n n N φ k N
30 26 29 bitri k n φ n N φ k N
31 sbsbc k n A S [˙k / n]˙ A S
32 sbcel1g k V [˙k / n]˙ A S k / n A S
33 32 elv [˙k / n]˙ A S k / n A S
34 nfcv _ k A
35 34 1 2 cbvcsbw k / n A = k / k B
36 csbid k / k B = B
37 35 36 eqtri k / n A = B
38 37 eleq1i k / n A S B S
39 31 33 38 3bitri k n A S B S
40 25 30 39 3imtr3i φ k N B S
41 11 24 40 syl2anc φ n N k 1 ..^ n B S
42 41 ralrimiva φ n N k 1 ..^ n B S
43 sigaclfu2 S ran sigAlgebra k 1 ..^ n B S k 1 ..^ n B S
44 10 42 43 syl2anc φ n N k 1 ..^ n B S
45 difelsiga S ran sigAlgebra A S k 1 ..^ n B S A k 1 ..^ n B S
46 10 5 44 45 syl3anc φ n N A k 1 ..^ n B S
47 46 ralrimiva φ n N A k 1 ..^ n B S
48 eqimss N = N
49 fzossnn 1 ..^ I
50 sseq1 N = 1 ..^ I N 1 ..^ I
51 49 50 mpbiri N = 1 ..^ I N
52 48 51 jaoi N = N = 1 ..^ I N
53 3 52 syl φ N
54 nnct ω
55 ssct N ω N ω
56 53 54 55 sylancl φ N ω
57 1 2 3 iundisj2cnt φ Disj n N A k 1 ..^ n B
58 measvuni M measures S n N A k 1 ..^ n B S N ω Disj n N A k 1 ..^ n B M n N A k 1 ..^ n B = * n N M A k 1 ..^ n B
59 4 47 56 57 58 syl112anc φ M n N A k 1 ..^ n B = * n N M A k 1 ..^ n B
60 7 59 eqtrd φ M n N A = * n N M A k 1 ..^ n B