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 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑀 ‘ 𝐴 ) = ( ( 𝑀 ‘ 𝐵 ) +𝑒 ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ) )

Proof

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