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 
|- F/_ n B
measiuns.1 
|- ( n = k -> A = B )
measiuns.2 
|- ( ph -> ( N = NN \/ N = ( 1 ..^ I ) ) )
measiuns.3 
|- ( ph -> M e. ( measures ` S ) )
measiuns.4 
|- ( ( ph /\ n e. N ) -> A e. S )
Assertion measiuns 
|- ( ph -> ( M ` U_ n e. N A ) = sum* n e. N ( M ` ( A \ U_ k e. ( 1 ..^ n ) B ) ) )

Proof

Step Hyp Ref Expression
1 measiuns.0 
 |-  F/_ n B
2 measiuns.1 
 |-  ( n = k -> A = B )
3 measiuns.2 
 |-  ( ph -> ( N = NN \/ N = ( 1 ..^ I ) ) )
4 measiuns.3 
 |-  ( ph -> M e. ( measures ` S ) )
5 measiuns.4 
 |-  ( ( ph /\ n e. N ) -> A e. S )
6 1 2 3 iundisjcnt 
 |-  ( ph -> U_ n e. N A = U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
7 6 fveq2d 
 |-  ( ph -> ( M ` U_ n e. N A ) = ( M ` U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
8 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
9 4 8 syl 
 |-  ( ph -> S e. U. ran sigAlgebra )
10 9 adantr 
 |-  ( ( ph /\ n e. N ) -> S e. U. ran sigAlgebra )
11 simpll 
 |-  ( ( ( ph /\ n e. N ) /\ k e. ( 1 ..^ n ) ) -> ph )
12 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
13 simpr 
 |-  ( ( ( ph /\ n e. N ) /\ N = NN ) -> N = NN )
14 12 13 sseqtrrid 
 |-  ( ( ( ph /\ n e. N ) /\ N = NN ) -> ( 1 ..^ n ) C_ N )
15 simplr 
 |-  ( ( ( ph /\ n e. N ) /\ N = ( 1 ..^ I ) ) -> n e. N )
16 simpr 
 |-  ( ( ( ph /\ n e. N ) /\ N = ( 1 ..^ I ) ) -> N = ( 1 ..^ I ) )
17 15 16 eleqtrd 
 |-  ( ( ( ph /\ n e. N ) /\ N = ( 1 ..^ I ) ) -> n e. ( 1 ..^ I ) )
18 elfzouz2 
 |-  ( n e. ( 1 ..^ I ) -> I e. ( ZZ>= ` n ) )
19 fzoss2 
 |-  ( I e. ( ZZ>= ` n ) -> ( 1 ..^ n ) C_ ( 1 ..^ I ) )
20 17 18 19 3syl 
 |-  ( ( ( ph /\ n e. N ) /\ N = ( 1 ..^ I ) ) -> ( 1 ..^ n ) C_ ( 1 ..^ I ) )
21 20 16 sseqtrrd 
 |-  ( ( ( ph /\ n e. N ) /\ N = ( 1 ..^ I ) ) -> ( 1 ..^ n ) C_ N )
22 3 adantr 
 |-  ( ( ph /\ n e. N ) -> ( N = NN \/ N = ( 1 ..^ I ) ) )
23 14 21 22 mpjaodan 
 |-  ( ( ph /\ n e. N ) -> ( 1 ..^ n ) C_ N )
24 23 sselda 
 |-  ( ( ( ph /\ n e. N ) /\ k e. ( 1 ..^ n ) ) -> k e. N )
25 5 sbimi 
 |-  ( [ k / n ] ( ph /\ n e. N ) -> [ k / n ] A e. S )
26 sban 
 |-  ( [ k / n ] ( ph /\ n e. N ) <-> ( [ k / n ] ph /\ [ k / n ] n e. N ) )
27 sbv 
 |-  ( [ k / n ] ph <-> ph )
28 clelsb3 
 |-  ( [ k / n ] n e. N <-> k e. N )
29 27 28 anbi12i 
 |-  ( ( [ k / n ] ph /\ [ k / n ] n e. N ) <-> ( ph /\ k e. N ) )
30 26 29 bitri 
 |-  ( [ k / n ] ( ph /\ n e. N ) <-> ( ph /\ k e. N ) )
31 sbsbc 
 |-  ( [ k / n ] A e. S <-> [. k / n ]. A e. S )
32 sbcel1g 
 |-  ( k e. _V -> ( [. k / n ]. A e. S <-> [_ k / n ]_ A e. S ) )
33 32 elv 
 |-  ( [. k / n ]. A e. S <-> [_ k / n ]_ A e. S )
34 nfcv 
 |-  F/_ 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 e. S <-> B e. S )
39 31 33 38 3bitri 
 |-  ( [ k / n ] A e. S <-> B e. S )
40 25 30 39 3imtr3i 
 |-  ( ( ph /\ k e. N ) -> B e. S )
41 11 24 40 syl2anc 
 |-  ( ( ( ph /\ n e. N ) /\ k e. ( 1 ..^ n ) ) -> B e. S )
42 41 ralrimiva 
 |-  ( ( ph /\ n e. N ) -> A. k e. ( 1 ..^ n ) B e. S )
43 sigaclfu2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ n ) B e. S ) -> U_ k e. ( 1 ..^ n ) B e. S )
44 10 42 43 syl2anc 
 |-  ( ( ph /\ n e. N ) -> U_ k e. ( 1 ..^ n ) B e. S )
45 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ U_ k e. ( 1 ..^ n ) B e. S ) -> ( A \ U_ k e. ( 1 ..^ n ) B ) e. S )
46 10 5 44 45 syl3anc 
 |-  ( ( ph /\ n e. N ) -> ( A \ U_ k e. ( 1 ..^ n ) B ) e. S )
47 46 ralrimiva 
 |-  ( ph -> A. n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) e. S )
48 eqimss 
 |-  ( N = NN -> N C_ NN )
49 fzossnn 
 |-  ( 1 ..^ I ) C_ NN
50 sseq1 
 |-  ( N = ( 1 ..^ I ) -> ( N C_ NN <-> ( 1 ..^ I ) C_ NN ) )
51 49 50 mpbiri 
 |-  ( N = ( 1 ..^ I ) -> N C_ NN )
52 48 51 jaoi 
 |-  ( ( N = NN \/ N = ( 1 ..^ I ) ) -> N C_ NN )
53 3 52 syl 
 |-  ( ph -> N C_ NN )
54 nnct 
 |-  NN ~<_ _om
55 ssct 
 |-  ( ( N C_ NN /\ NN ~<_ _om ) -> N ~<_ _om )
56 53 54 55 sylancl 
 |-  ( ph -> N ~<_ _om )
57 1 2 3 iundisj2cnt 
 |-  ( ph -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
58 measvuni 
 |-  ( ( M e. ( measures ` S ) /\ A. n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) e. S /\ ( N ~<_ _om /\ Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) ) ) -> ( M ` U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) ) = sum* n e. N ( M ` ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
59 4 47 56 57 58 syl112anc 
 |-  ( ph -> ( M ` U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) ) = sum* n e. N ( M ` ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
60 7 59 eqtrd 
 |-  ( ph -> ( M ` U_ n e. N A ) = sum* n e. N ( M ` ( A \ U_ k e. ( 1 ..^ n ) B ) ) )