Metamath Proof Explorer

Theorem measxun2

Description: The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017)

Ref Expression
Assertion measxun2 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ A = M ⁡ B + 𝑒 M ⁡ A ∖ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ∈ measures ⁡ S
2 simp2r ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B ∈ S
3 measbase ⊢ M ∈ measures ⁡ S → S ∈ ⋃ ran ⁡ sigAlgebra
4 1 3 syl ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → S ∈ ⋃ ran ⁡ sigAlgebra
5 simp2l ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → A ∈ S
6 difelsiga ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ A ∈ S ∧ B ∈ S → A ∖ B ∈ S
7 4 5 2 6 syl3anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → A ∖ B ∈ S
8 prelpwi ⊢ B ∈ S ∧ A ∖ B ∈ S → B A ∖ B ∈ 𝒫 S
9 2 7 8 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B A ∖ B ∈ 𝒫 S
10 prct ⊢ B ∈ S ∧ A ∖ B ∈ S → B A ∖ B ≼ ω
11 2 7 10 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B A ∖ B ≼ ω
12 simp3 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B ⊆ A
13 disjdifprg2 ⊢ A ∈ S → Disj x ∈ A ∖ B A ∩ B x
14 prcom ⊢ A ∖ B B = B A ∖ B
15 dfss ⊢ B ⊆ A ↔ B = B ∩ A
16 15 biimpi ⊢ B ⊆ A → B = B ∩ A
17 incom ⊢ B ∩ A = A ∩ B
18 16 17 eqtrdi ⊢ B ⊆ A → B = A ∩ B
19 18 preq2d ⊢ B ⊆ A → A ∖ B B = A ∖ B A ∩ B
20 14 19 eqtr3id ⊢ B ⊆ A → B A ∖ B = A ∖ B A ∩ B
21 20 disjeq1d ⊢ B ⊆ A → Disj x ∈ B A ∖ B x ↔ Disj x ∈ A ∖ B A ∩ B x
22 21 biimprd ⊢ B ⊆ A → Disj x ∈ A ∖ B A ∩ B x → Disj x ∈ B A ∖ B x
23 13 22 mpan9 ⊢ A ∈ S ∧ B ⊆ A → Disj x ∈ B A ∖ B x
24 5 12 23 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → Disj x ∈ B A ∖ B x
25 11 24 jca ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B A ∖ B ≼ ω ∧ Disj x ∈ B A ∖ B x
26 measvun ⊢ M ∈ measures ⁡ S ∧ B A ∖ B ∈ 𝒫 S ∧ B A ∖ B ≼ ω ∧ Disj x ∈ B A ∖ B x → M ⁡ ⋃ B A ∖ B = ∑ * x ∈ B A ∖ B M ⁡ x
27 1 9 25 26 syl3anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ ⋃ B A ∖ B = ∑ * x ∈ B A ∖ B M ⁡ x
28 2 7 jca ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B ∈ S ∧ A ∖ B ∈ S
29 uniprg ⊢ B ∈ S ∧ A ∖ B ∈ S → ⋃ B A ∖ B = B ∪ A ∖ B
30 undif ⊢ B ⊆ A ↔ B ∪ A ∖ B = A
31 30 biimpi ⊢ B ⊆ A → B ∪ A ∖ B = A
32 29 31 sylan9eq ⊢ B ∈ S ∧ A ∖ B ∈ S ∧ B ⊆ A → ⋃ B A ∖ B = A
33 32 fveq2d ⊢ B ∈ S ∧ A ∖ B ∈ S ∧ B ⊆ A → M ⁡ ⋃ B A ∖ B = M ⁡ A
34 28 12 33 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ ⋃ B A ∖ B = M ⁡ A
35 simpr ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ x = B → x = B
36 35 fveq2d ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ x = B → M ⁡ x = M ⁡ B
37 simpr ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ x = A ∖ B → x = A ∖ B
38 37 fveq2d ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ x = A ∖ B → M ⁡ x = M ⁡ A ∖ B
39 measvxrge0 ⊢ M ∈ measures ⁡ S ∧ B ∈ S → M ⁡ B ∈ 0 +∞
40 1 2 39 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ B ∈ 0 +∞
41 measvxrge0 ⊢ M ∈ measures ⁡ S ∧ A ∖ B ∈ S → M ⁡ A ∖ B ∈ 0 +∞
42 1 7 41 syl2anc ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ A ∖ B ∈ 0 +∞
43 eqimss ⊢ B = A ∖ B → B ⊆ A ∖ B
44 ssdifeq0 ⊢ B ⊆ A ∖ B ↔ B = ∅
45 43 44 sylib ⊢ B = A ∖ B → B = ∅
46 45 fveq2d ⊢ B = A ∖ B → M ⁡ B = M ⁡ ∅
47 measvnul ⊢ M ∈ measures ⁡ S → M ⁡ ∅ = 0
48 46 47 sylan9eqr ⊢ M ∈ measures ⁡ S ∧ B = A ∖ B → M ⁡ B = 0
49 1 48 sylan ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ B = A ∖ B → M ⁡ B = 0
50 49 orcd ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A ∧ B = A ∖ B → M ⁡ B = 0 ∨ M ⁡ B = +∞
51 50 ex ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → B = A ∖ B → M ⁡ B = 0 ∨ M ⁡ B = +∞
52 36 38 2 7 40 42 51 esumpr2 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → ∑ * x ∈ B A ∖ B M ⁡ x = M ⁡ B + 𝑒 M ⁡ A ∖ B
53 27 34 52 3eqtr3d ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ B ∈ S ∧ B ⊆ A → M ⁡ A = M ⁡ B + 𝑒 M ⁡ A ∖ B