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 ⊢ Ⅎ 𝑛 𝐵
measiuns.1 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
measiuns.2 ⊢ ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝐼 ) ) )
measiuns.3 ⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
measiuns.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ∈ 𝑆 )
Assertion measiuns ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 𝐴 ) = Σ* 𝑛 ∈ 𝑁 ( 𝑀 ‘ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 measiuns.0 ⊢ Ⅎ 𝑛 𝐵
2 measiuns.1 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
3 measiuns.2 ⊢ ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝐼 ) ) )
4 measiuns.3 ⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
5 measiuns.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ∈ 𝑆 )
6 1 2 3 iundisjcnt ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
7 6 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 𝐴 ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
8 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
9 4 8 syl ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝑆 ∈ ∪ ran sigAlgebra )
11 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝜑 )
12 fzossnn ⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ℕ ) → 𝑁 = ℕ )
14 12 13 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ℕ ) → ( 1 ..^ 𝑛 ) ⊆ 𝑁 )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ( 1 ..^ 𝐼 ) ) → 𝑛 ∈ 𝑁 )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ( 1 ..^ 𝐼 ) ) → 𝑁 = ( 1 ..^ 𝐼 ) )
17 15 16 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ( 1 ..^ 𝐼 ) ) → 𝑛 ∈ ( 1 ..^ 𝐼 ) )
18 elfzouz2 ⊢ ( 𝑛 ∈ ( 1 ..^ 𝐼 ) → 𝐼 ∈ ( ℤ≥ ‘ 𝑛 ) )
19 fzoss2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 1 ..^ 𝑛 ) ⊆ ( 1 ..^ 𝐼 ) )
20 17 18 19 3syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ( 1 ..^ 𝐼 ) ) → ( 1 ..^ 𝑛 ) ⊆ ( 1 ..^ 𝐼 ) )
21 20 16 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑁 = ( 1 ..^ 𝐼 ) ) → ( 1 ..^ 𝑛 ) ⊆ 𝑁 )
22 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝐼 ) ) )
23 14 21 22 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( 1 ..^ 𝑛 ) ⊆ 𝑁 )
24 23 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ 𝑁 )
25 5 sbimi ⊢ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 )
26 sban ⊢ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ↔ ( [ 𝑘 / 𝑛 ] 𝜑 ∧ [ 𝑘 / 𝑛 ] 𝑛 ∈ 𝑁 ) )
27 sbv ⊢ ( [ 𝑘 / 𝑛 ] 𝜑 ↔ 𝜑 )
28 clelsb1 ⊢ ( [ 𝑘 / 𝑛 ] 𝑛 ∈ 𝑁 ↔ 𝑘 ∈ 𝑁 )
29 27 28 anbi12i ⊢ ( ( [ 𝑘 / 𝑛 ] 𝜑 ∧ [ 𝑘 / 𝑛 ] 𝑛 ∈ 𝑁 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑁 ) )
30 26 29 bitri ⊢ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑁 ) )
31 sbsbc ⊢ ( [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 ↔ [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 )
32 sbcel1g ⊢ ( 𝑘 ∈ V → ( [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ 𝑆 ) )
33 32 elv ⊢ ( [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ 𝑆 )
34 nfcv ⊢ Ⅎ 𝑘 𝐴
35 34 1 2 cbvcsbw ⊢ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵
36 csbid ⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = 𝐵
37 35 36 eqtri ⊢ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = 𝐵
38 37 eleq1i ⊢ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 )
39 31 33 38 3bitri ⊢ ( [ 𝑘 / 𝑛 ] 𝐴 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 )
40 25 30 39 3imtr3i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ) → 𝐵 ∈ 𝑆 )
41 11 24 40 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝐵 ∈ 𝑆 )
42 41 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 )
43 sigaclfu2 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 )
44 10 42 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 )
45 difelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∈ 𝑆 )
46 10 5 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∈ 𝑆 )
47 46 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∈ 𝑆 )
48 eqimss ⊢ ( 𝑁 = ℕ → 𝑁 ⊆ ℕ )
49 fzossnn ⊢ ( 1 ..^ 𝐼 ) ⊆ ℕ
50 sseq1 ⊢ ( 𝑁 = ( 1 ..^ 𝐼 ) → ( 𝑁 ⊆ ℕ ↔ ( 1 ..^ 𝐼 ) ⊆ ℕ ) )
51 49 50 mpbiri ⊢ ( 𝑁 = ( 1 ..^ 𝐼 ) → 𝑁 ⊆ ℕ )
52 48 51 jaoi ⊢ ( ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝐼 ) ) → 𝑁 ⊆ ℕ )
53 3 52 syl ⊢ ( 𝜑 → 𝑁 ⊆ ℕ )
54 nnct ⊢ ℕ ≼ ω
55 ssct ⊢ ( ( 𝑁 ⊆ ℕ ∧ ℕ ≼ ω ) → 𝑁 ≼ ω )
56 53 54 55 sylancl ⊢ ( 𝜑 → 𝑁 ≼ ω )
57 1 2 3 iundisj2cnt ⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
58 measvuni ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∈ 𝑆 ∧ ( 𝑁 ≼ ω ∧ Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = Σ* 𝑛 ∈ 𝑁 ( 𝑀 ‘ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
59 4 47 56 57 58 syl112anc ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = Σ* 𝑛 ∈ 𝑁 ( 𝑀 ‘ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
60 7 59 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑁 𝐴 ) = Σ* 𝑛 ∈ 𝑁 ( 𝑀 ‘ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )